This book constitutes the refereed proceedings of the 20th International Conference on Automated Deduction, CADE-20, held in Tallinn, Estonia, in July 2005.
The 25 revised full papers and 5 system descriptions presented were carefully reviewed and selected from 78 submissions. All current aspects of automated deduction are addressed, ranging from theoretical and methodological issues to presentation and evaluation of theorem provers and logical reasoning systems.
Author(s): Gilles Dowek (auth.), Robert Nieuwenhuis (eds.)
Series: Lecture Notes in Computer Science 3632 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2005
Language: English
Pages: 466
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Software Engineering
Front Matter....Pages -
What Do We Know When We Know That a Theory Is Consistent?....Pages 1-6
Reflecting Proofs in First-Order Logic with Equality....Pages 7-22
Reasoning in Extensional Type Theory with Equality....Pages 23-37
Nominal Techniques in Isabelle/HOL....Pages 38-53
Tabling for Higher-Order Logic Programming....Pages 54-68
A Focusing Inverse Method Theorem Prover for First-Order Linear Logic....Pages 69-83
The CoRe Calculus....Pages 84-98
Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures....Pages 99-115
Privacy-Sensitive Information Flow with JML....Pages 116-130
The Decidability of the First-Order Theory of Knuth-Bendix Order....Pages 131-148
Well-Nested Context Unification....Pages 149-163
Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules....Pages 164-176
The OWL Instance Store: System Description....Pages 177-181
Temporal Logics over Transitive States....Pages 182-203
Deciding Monodic Fragments by Temporal Resolution....Pages 204-218
Hierarchic Reasoning in Local Theory Extensions....Pages 219-234
Proof Planning for First-Order Temporal Logic....Pages 235-249
System Description: Multi A Multi-strategy Proof Planner....Pages 250-254
Decision Procedures Customized for Formal Verification....Pages 255-259
An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic....Pages 260-277
Connecting Many-Sorted Theories....Pages 278-294
A Proof-Producing Decision Procedure for Real Arithmetic....Pages 295-314
The MathSAT 3 System....Pages 315-321
Deduction with XOR Constraints in Security API Modelling....Pages 322-336
On the Complexity of Equational Horn Clauses....Pages 337-352
A Combination Method for Generating Interpolants....Pages 353-368
sKizzo: A Suite to Evaluate and Certify QBFs....Pages 369-376
Regular Protocols and Attacks with Regular Knowledge....Pages 377-391
The Model Evolution Calculus with Equality....Pages 392-408
Model Representation via Contexts and Implicit Generalizations....Pages 409-423
Proving Properties of Incremental Merkle Trees....Pages 424-440
Computer Search for Counterexamples to Wilkie’s Identity....Pages 441-451
KRHyper – In Your Pocket....Pages 452-457
Back Matter....Pages -
