Automated Deduction - CADE-19: 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings (Lecture ... / Lecture Notes in Artificial Intelligence)

This volume contains the papers presented at the 19th International Conference on Automated Deduction (CADE-19) held 28 July–2 August 2003 in Miami Beach, Florida, USA. They are divided into the following categories: – 4 contributions by invited speakers: one full paper and three short abstracts; – 29 accepted technical papers; – 7 descriptions of automated reasoning systems. These proceedings also contain a short description of the automated theor- proving system competition (CASC-19) organized by Geo? Sutcli?e and Chr- tian Suttner. Despite many competing smaller conferences and workshops covering di?- entaspectsofautomateddeduction,CADEisstillthemajorforumfordiscussing new results on all aspects of automated deduction as well as presenting new s- tems and improvements of established systems. In contrast to the previous year, when CADE was one of the conferences participating in the Third Federated Logic Conference (FLoC 2002), and next year, when CADE will be part of the Second International Joint Conference on Automated Reasoning (IJCAR 2004), CADE-19 was organized as a stand-alone event. Front Matter....Pages - SAT-Based Counterexample Guided Abstraction Refinement in Model Checking....Pages 1-1 Equational Abstractions....Pages 2-16 Deciding Inductive Validity of Equations....Pages 17-31 Automating the Dependency Pair Method....Pages 32-46 An AC-Compatible Knuth-Bendix Order....Pages 47-59 The Complexity of Finite Model Reasoning in Description Logics....Pages 60-74 Optimizing a BDD-Based Modal Solver....Pages 75-89 A Translation of Looping Alternating Automata into Description Logics....Pages 90-105 Foundational Certified Code in a Metalogical Framework....Pages 106-120 Proving Pointer Programs in Higher-Order Logic....Pages 121-135 ⋌....Pages 136-150 Subset Types and Partial Functions....Pages 151-165 Reasoning about Quantifiers by Matching in the E-graph....Pages 166-166 A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols....Pages 167-181 Superposition Modulo a Shostak Theory....Pages 182-196 Canonization for Disjoint Unions of Theories....Pages 197-211 Matching in a Class of Combined Non-disjoint Theories....Pages 212-227 Reasoning about Iteration in Gödel’s Class Theory....Pages 228-242 Algorithms for Ordinal Arithmetic....Pages 243-257 Certifying Solutions to Permutation Group Problems....Pages 258-273 TRP++ 2.0: A Temporal Resolution Prover....Pages 274-278 IsaPlanner: A Prototype Proof Planner in Isabelle....Pages 279-283 ’Living Book’ :- ’Deduction’, ’Slicing’, ’Interaction’ ....Pages 284-288 The Homer System....Pages 289-294 The CADE-19 ATP System Competition....Pages 295-296 Proof Search and Proof Check for Equational and Inductive Theorems....Pages 297-316 The New WALDMEISTER Loop at Work....Pages 317-321 About VeriFun....Pages 322-327 How to Prove Inductive Theorems? QuodLibet !....Pages 328-333 Reasoning about Qualitative Representations of Space and Time....Pages 334-334 Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation....Pages 335-349 The Model Evolution Calculus....Pages 350-364 Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms....Pages 365-379 Efficient Instance Retrieval with Standard and Relational Path Indexing....Pages 380-396 Monodic Temporal Resolution....Pages 397-411 A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae....Pages 412-426 Schematic Saturation for Decision and Unification Problems....Pages 427-441 Unification Modulo ACUI Plus Homomorphisms/Distributivity....Pages 442-457 Source-Tracking Unification....Pages 458-472 Optimizing Higher-Order Pattern Unification....Pages 473-487 Decidability of Arity-Bounded Higher-Order Matching....Pages 488-502 Back Matter....Pages -

This book constitutes the refereed proceedings of the 19th International Conference on Automated Deduction, CADE 2003, held in Miami Beach, FL, USA in July 2003.

The 29 revised full papers and 7 system description papers presented together with an invited paper and 3 abstracts of invited talks were carefully reviewed and selected from 83 submissions. All current aspects of automated deduction are discussed, ranging from theoretical and methodological issues to the presentation of new theorem provers and systems.

This book constitutes the refereed proceedings of the 19th International Conference on Automated Deduction, CADE 2003, held in Miami Beach, FL, USA in July 2003. The 29 revised full papers and 7 system description papers presented together with an invited paper and 3 abstracts of invited talks were carefully reviewed and selected from 83 submissions. All current aspects of automated deduction are discussed, ranging from theoretical and methodological issues to the presentation of new theorem provers and systems