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.
Author(s): Edmund M. Clarke (auth.), Franz Baader (eds.)
Series: Lecture Notes in Computer Science 2741 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2003
Language: English
Pages: 512
Tags: Artificial Intelligence (incl. Robotics); Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs; Mathematical Logic and Formal Languages
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 -
