Automated Deduction CADE-20 自动化演绎－CADE-20/2005年国际会议录

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.

What Do We Know When We Know That a Theory Is Consistent?
Reflecting Proofs in First-Order Logic with Equality
Reasoning in Extensional Type Theory with Equality
Nominal Techniques in Isabelle/HOL
Tabling for Higher-Order Logic Programming
A Focusing Inverse Method Theorem Prover for First-Order Linear Logic
The CoRE Calculus
Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures
Privacy-Sensitive Information Flow with JML
The Decidability of the First-Order Theory of Knuth-Bendix Order
Well-Nested Context Unification
Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules
The OWL Instance Store: System Description
Temporal Logics over Transitive States
Deciding Monodic Fragments by Temporal Resolution
Hierarchic Reasoning in Local Theory Extensions
Proof Planning for First-Order Temporal Logic
System Description: MULTI A Multi-strategy Proof Planner
Decision Procedures Customized for Formal Verification
An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
Connecting Many-Sorted Theories
A Proof-Producing Decision Procedure for Real Arithmetic
The MathSAT 3 System
Deduction with XOR Constraints in Security API Modelling
On the Complexity of Equational Horn Clauses
A Combination Method for Generating Interpolants
sKizzo: A Suite to Evaluate and Certify QBFs
……
Author Index