Automated Deduction – CADE-19 : 19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28 – August 2, 2003. Proceedings

Table of Contents

1. Altmetric Badge
   Book Overview
2. Altmetric Badge
   Chapter 1 SAT-Based Counterexample Guided Abstraction Refinement in Model Checking
3. Altmetric Badge
   Chapter 2 Equational Abstractions
4. Altmetric Badge
   Chapter 3 Deciding Inductive Validity of Equations
5. Altmetric Badge
   Chapter 4 Automating the Dependency Pair Method
6. Altmetric Badge
   Chapter 5 An AC-Compatible Knuth-Bendix Order
7. Altmetric Badge
   Chapter 6 The Complexity of Finite Model Reasoning in Description Logics
8. Altmetric Badge
   Chapter 7 Optimizing a BDD-Based Modal Solver
9. Altmetric Badge
   Chapter 8 A Translation of Looping Alternating Automata into Description Logics
10. Altmetric Badge
    Chapter 9 Automated Deduction – CADE-19
11. Altmetric Badge
    Chapter 10 Proving Pointer Programs in Higher-Order Logic
12. Altmetric Badge
    Chapter 11 ⋌
13. Altmetric Badge
    Chapter 12 Subset Types and Partial Functions
14. Altmetric Badge
    Chapter 13 Reasoning about Quantifiers by Matching in the E-graph
15. Altmetric Badge
    Chapter 14 A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols
16. Altmetric Badge
    Chapter 15 Superposition Modulo a Shostak Theory
17. Altmetric Badge
    Chapter 16 Canonization for Disjoint Unions of Theories
18. Altmetric Badge
    Chapter 17 Matching in a Class of Combined Non-disjoint Theories
19. Altmetric Badge
    Chapter 18 Reasoning about Iteration in Gödel’s Class Theory
20. Altmetric Badge
    Chapter 19 Algorithms for Ordinal Arithmetic
21. Altmetric Badge
    Chapter 20 Certifying Solutions to Permutation Group Problems
22. Altmetric Badge
    Chapter 21 TRP++ 2.0: A Temporal Resolution Prover
23. Altmetric Badge
    Chapter 22 IsaPlanner: A Prototype Proof Planner in Isabelle
24. Altmetric Badge
    Chapter 23 ’Living Book’ :- ’Deduction’, ’Slicing’, ’Interaction’
25. Altmetric Badge
    Chapter 24 The Homer System
26. Altmetric Badge
    Chapter 25 The CADE-19 ATP System Competition
27. Altmetric Badge
    Chapter 26 Proof Search and Proof Check for Equational and Inductive Theorems
28. Altmetric Badge
    Chapter 27 The New WALDMEISTER Loop at Work
29. Altmetric Badge
    Chapter 28 About VeriFun
30. Altmetric Badge
    Chapter 29 How to Prove Inductive Theorems? QuodLibet !
31. Altmetric Badge
    Chapter 30 Reasoning about Qualitative Representations of Space and Time
32. Altmetric Badge
    Chapter 31 Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
33. Altmetric Badge
    Chapter 32 The Model Evolution Calculus
34. Altmetric Badge
    Chapter 33 Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
35. Altmetric Badge
    Chapter 34 Efficient Instance Retrieval with Standard and Relational Path Indexing
36. Altmetric Badge
    Chapter 35 Monodic Temporal Resolution
37. Altmetric Badge
    Chapter 36 A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae
38. Altmetric Badge
    Chapter 37 Schematic Saturation for Decision and Unification Problems
39. Altmetric Badge
    Chapter 38 Unification Modulo ACUI Plus Homomorphisms/Distributivity
40. Altmetric Badge
    Chapter 39 Source-Tracking Unification
41. Altmetric Badge
    Chapter 40 Optimizing Higher-Order Pattern Unification
42. Altmetric Badge
    Chapter 41 Decidability of Arity-Bounded Higher-Order Matching