Automated Deduction – CADE-21: 21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings

Cover
......Page 1
Automated Deduction – CADE-21: 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007 Proceedings......Page 3
ISBN-10 3540735941  ISBN-13 9783540735946......Page 4
Preface......Page 5
Conference Organization......Page 6
Table of Contents......Page 8
Games, Automata and Matching......Page 12
Introduction......Page 14
Verifying Probabilistic Algorithms in HOL......Page 16
Formal Specification of Standard Uniform Random Variable......Page 17
Formal Verification of Standard Uniform Random Variable......Page 18
Formal Verification of CDF Properties......Page 19
Formal Specification of the Inverse Transform method......Page 21
Formal Verification of the Inverse Transform Method......Page 22
Formalization of Continuous Probability Distributions......Page 23
Formal Verification of Continuous Random Variables......Page 24
Applications......Page 26
Related Work......Page 27
Conclusions......Page 28
Introduction......Page 30
Motivation......Page 31
Compilation by Proof......Page 33
Normalization......Page 34
Transformations of Normal Forms......Page 35
Closure Conversion......Page 36
Register Allocation......Page 37
Structured Assembly Language......Page 39
Machine Code Generation......Page 42
Related Work......Page 43
Summary and Future Work......Page 44
Introduction......Page 46
Nominal Logic......Page 50
Schematic Terms and Schematic Rules......Page 52
Strengthening of the Induction Principle......Page 54
Simple Typing......Page 56
Parallel Reduction......Page 58
Related Work......Page 59
Conclusion......Page 60
Introduction......Page 62
Example......Page 63
Detailed Procedure......Page 64
Soundness......Page 65
Completeness over All Rings......Page 66
Reduction to Standard Form......Page 70
Introduction of GCDs......Page 72
Sequential Treatment of Equations......Page 73
Implementation......Page 74
Conclusions and Related Work......Page 75
Introduction......Page 78
Preliminaries......Page 79
Algorithm Overview......Page 80
Preprocessing......Page 82
The Hypertableau Calculus for DL-Clauses......Page 85
Applying the Algorithm to Other DLs......Page 90
Implementation......Page 91
Conclusion......Page 92
Introduction......Page 95
$EL$ and Conservative Extensions......Page 97
Characterizing Conservative Extensions......Page 98
The Algorithm......Page 101
$EXPTIME$-Hardness......Page 103
Model Conservativity......Page 106
Conclusion......Page 109
Introduction......Page 111
$\\mu$-Calculus......Page 112
Alternating Automata......Page 113
From APT to NBT Via UCT......Page 114
Decomposition of the APT to NBT Translation......Page 116
The Algorithm......Page 119
A Top-Down Approach to the APT to NBT Translation and to the NBT Emptiness Algorithm......Page 120
Heuristics......Page 121
Conclusions and Future Work......Page 124
Introduction......Page 127
Natural Deduction......Page 128
Sequent Calculi......Page 130
Bidirectional Proof Search in Sequent Calculus......Page 134
Bidirectional Proof Search in Natural Deduction......Page 138
Experimental Results......Page 140
Related and Future Work......Page 141
Introduction......Page 143
Language, Indexing and Derivations......Page 144
Variable Splitting and Admissibility......Page 147
Labelled Formulas and Semantics......Page 149
Soundness......Page 150
Completeness and Termination......Page 151
Conclusion and Future Work......Page 156
Introduction......Page 158
Problem Definition......Page 159
Program Model......Page 160
Abstract Interpretation......Page 161
The Assertion Checking Problem......Page 162
Logical Interpretation......Page 163
The Theory of Uninterpreted Symbols......Page 164
The Theory of Linear Arithmetic......Page 165
Checking Disequality Assertions Is Intractable......Page 166
Checking Disjunctive Assertions......Page 167
Bitary Theories......Page 168
Revisiting the Combined Theory of $UFS+LAE$......Page 169
Interprocedural Logical Interpretation......Page 170
The Theory of Unary Uninterpreted Symbols......Page 171
Unitary Theories......Page 172
Forward Abstract Interpretation over Logical Lattices......Page 173
Richer Logical Lattices......Page 174
Interface for a Logical Lattice: The Boolean Interface......Page 175
Conclusion......Page 176
Introduction......Page 178
Background......Page 179
Reasoning with Quantifiers in SMT......Page 180
Modeling Quantifier Instantiation......Page 181
Instantiation Via Matching......Page 182
Improving Instantiation Strategies......Page 183
Triggers......Page 184
Matching Algorithm......Page 185
Trigger Matching by Instantiation Levels......Page 186
Benchmarks......Page 187
Evaluating the Heuristics......Page 189
Comparison with ATP Systems......Page 190
Comparison with Other SMT Systems......Page 191
Conclusion......Page 192
Introduction......Page 194
Background......Page 195
SMT Solvers......Page 196
E-Matching Abstract Machine......Page 197
E-Matching Code Trees......Page 198
Incrementality......Page 201
Inverted Path Index......Page 202
Filters......Page 203
Implementation Issues......Page 204
Experiments......Page 206
Conclusion......Page 208
Introduction......Page 210
Preliminaries......Page 212
The Decomposition Framework......Page 213
Supported Strategies and $\\presth{T}$-Compatibility......Page 214
Preserving $\\presth{T}$-Compatibility......Page 215
$\\presth{T}$-Stability......Page 217
$\\presth{T}$-Decision Procedures Based on $SP$......Page 218
Some $\\presth{T}$-Stable Sets......Page 219
The Theory of Records......Page 220
The Theory of Integer Offsets......Page 221
The Theory of Arrays......Page 222
Discussion......Page 223
Introduction......Page 226
Challenges in Checking $QFBAPA$ Satisfiability......Page 227
Our Results......Page 229
Constructing Small Presburger Arithmetic Formulas......Page 230
Upper Bound on the Number of Non-zero Regions......Page 232
Bounds and Nonredundant Integer Cone Generators......Page 233
Lower Bounds......Page 235
Better Upper Bounds for Small Cardinalities......Page 237
Preliminary Experiments......Page 238
Related Work......Page 239
Introduction......Page 242
Inverse Substitution: Selector Elimination......Page 245
Inverse Substitution: Common Non-Variable Subterms......Page 247
Inverse Substitution: Generalizing Apart Variables......Page 249
Inverse Functionality......Page 252
Related Work......Page 253
Evaluation of the Generalization Heuristics......Page 254
Conclusion......Page 256
Introduction......Page 258
Preliminaries......Page 259
Simplifying Assumptions......Page 261
Rewrite Closure......Page 262
Characterization......Page 263
Characterizing Normalization of Flat Right-Linear TRS......Page 265
The Right-Flat Linear Case......Page 267
The Flat Right-Linear Case......Page 268
Undecidability of Unique Normalization in the Linear Right-Shallow Case......Page 272
Introduction......Page 274
Preliminaries......Page 275
Reduction to Unsorted Logic......Page 277
Translation......Page 278
Translation Proofs......Page 280
Translation......Page 284
Translation Proofs......Page 285
Experiments......Page 286
Related Works and Conclusion......Page 287
Introduction......Page 290
Idempotent Semirings......Page 292
Iteration Algebras......Page 293
Automating Concurrency Control......Page 295
Automating Hoare Logic: A First Attempt......Page 296
Modal Semirings......Page 297
Automating Hoare Logic......Page 298
Automating Dynamic Logics......Page 300
Automating Linear Temporal Logics......Page 301
Automating Modal Correspondence Theory......Page 302
Conclusion......Page 303
Introduction......Page 306
The Basic Process......Page 307
The Extended Process......Page 309
Syntactic Relevance Ordering......Page 313
Results......Page 314
Conclusion......Page 319
Introduction......Page 322
Contributions......Page 324
Superposition with Labels......Page 325
Multiple Labelled Conjectures......Page 328
Labelled Splitting......Page 330
Slicing......Page 332
Cartesian Abstraction......Page 333
Shape Analysis and Canonical Abstraction......Page 334
Experiments......Page 335
Conclusion......Page 336
Introduction......Page 339
Preliminaries......Page 340
Paramodulation-Based Satisfiability Procedure......Page 341
Automatic Decidability......Page 343
Automatic Combinability......Page 349
Conclusion......Page 354
Designing Verification Conditions for Software......Page 356
Introduction......Page 357
Background......Page 359
Encoding of Temporal Properties......Page 362
Implicit Bound Encoding......Page 366
Encoding of the System Description......Page 367
Module Variables......Page 368
Submodel Instances......Page 369
Module References......Page 370
Conclusions and Future Work......Page 371
Introduction......Page 373
Background......Page 374
Temporal Logic......Page 376
The Satisfiability Problem......Page 378
The Model-Checking Problem......Page 381
Discussion......Page 386
The KeY System 1.0 (Deduction Component)......Page 390
Introduction......Page 396
C Dynamic Logic by Example......Page 397
Current Status and Further Work......Page 400
Related Work and Summary......Page 401
Foundations......Page 402
Architecture......Page 403
Examples......Page 405
Future Work......Page 407
Introduction......Page 409
ForTheL Language......Page 410
System for Automated Deduction......Page 411
Conclusion......Page 413
Instance Based Methods......Page 415
Logical Engineering......Page 416
Introduction......Page 421
Preliminaries......Page 422
Dependency Pairs......Page 423
Semantic and Predictive Labeling......Page 425
Predictive Labeling and Dependency Pairs......Page 426
SAT Encoding......Page 428
Experimental Results......Page 432
Conclusion and Further Research......Page 434
Introduction......Page 437
Equational Rewriting......Page 439
$S$-Normalized Rewriting......Page 441
Dependency Pairs......Page 443
Dependency Pair Framework......Page 445
DP Processors......Page 446
A DP Processor Based on Dependency Graphs......Page 447
A DP Processor Based on Removal of Rules......Page 448
A DP Processor Based on Narrowing......Page 449
Conclusions......Page 450
Propositional Sequent Calculus......Page 452
Introduction......Page 454
Dependency Pairs......Page 455
General Reduction Pairs......Page 457
Conditions for Bounded Increase......Page 461
Conclusion......Page 468
Size-Change Termination - Abstractly......Page 471
No Simple Certificates......Page 473
Related Work......Page 474
Graphs......Page 475
Size-Change Graphs......Page 476
Generating Size-Change Problems......Page 477
Call Descriptors......Page 478
Approximating the Control Graph......Page 479
Building Size-Change Problems......Page 480
Implementation Prototype......Page 481
Examples......Page 482
Practical Applications......Page 484
Conclusion......Page 485
Introduction......Page 487
Connection Tableaux......Page 489
Rigid Unsatisfiability......Page 490
Encoding for Horn Clauses......Page 491
Encoding for Non-horn Clauses......Page 492
Tableau Encoding Algorithm(TE)......Page 494
Completeness and Soundness Theorems for HTE......Page 495
Completeness and Soundness Theorems for NHTE......Page 498
CHEWTPTP Implementation......Page 499
Conclusion......Page 500
Introduction......Page 503
Preliminaries......Page 505
Inference Rules on Clauses......Page 507
Redundant Inferences and Saturation......Page 508
E-Hyper Tableaux......Page 510
Deletion and Simplification Rules......Page 511
Derivations......Page 513
Restricting Split and the Relation to Splitting in SPASS......Page 515
Implementation......Page 516
Conclusion......Page 517
Language, Usage and Availability......Page 519
Model Generation and Theorem Proving Method......Page 520
Related Systems and Performance Evaluation......Page 521
Conclusion......Page 522
Introduction......Page 525
Modal Logics, Relational Logics and Description Logics......Page 526
Renaming and Selection Enhancements......Page 528
Interface Enhancements......Page 529
Conclusion and Future Work......Page 530
Author Index......Page 532