Automated Deduction — Cade-13

Table of Contents

1. Altmetric Badge
   Book Overview
2. Altmetric Badge
   Chapter 64 Saturation-based theorem proving: Past successes and future potential
3. Altmetric Badge
   Chapter 65 A resolution theorem prover for intuitionistic logic
4. Altmetric Badge
   Chapter 66 Proof-terms for classical and intuitionistic resolution
5. Altmetric Badge
   Chapter 67 Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification
6. Altmetric Badge
   Chapter 68 Extensions to a generalization critic for inductive proof
7. Altmetric Badge
   Chapter 69 Learning domain knowledge to improve theorem proving
8. Altmetric Badge
   Chapter 70 Patching faulty conjectures
9. Altmetric Badge
   Chapter 71 Internal analogy in theorem proving
10. Altmetric Badge
    Chapter 72 Termination of theorem proving by reuse
11. Altmetric Badge
    Chapter 73 Termination of algorithms over non-freely generated data types
12. Altmetric Badge
    Chapter 74 ABSFOL: A proof checker with abstraction
13. Altmetric Badge
    Chapter 75 SPASS & FLOTTER version 0.42
14. Altmetric Badge
    Chapter 76 The design of the CADE-13 ATP system competition
15. Altmetric Badge
    Chapter 77 SCAN—Elimination of predicate quantifiers
16. Altmetric Badge
    Chapter 78 GEOTHER: A geometry theorem prover
17. Altmetric Badge
    Chapter 79 Structuring metatheory on inductive definitions
18. Altmetric Badge
    Chapter 80 An embedding of Ruby in Isabelle
19. Altmetric Badge
    Chapter 81 Mechanical verification of mutually recursive procedures
20. Altmetric Badge
    Chapter 82 FasTraC a decentralized traffic control system based on logic programming
21. Altmetric Badge
    Chapter 83 Presenting machine-found proofs
22. Altmetric Badge
    Chapter 84 MUltlog 1.0: Towards an expert system for many-valued logics
23. Altmetric Badge
    Chapter 85 CtCoq: A system presentation
24. Altmetric Badge
    Chapter 86 An introduction to geometry expert
25. Altmetric Badge
    Chapter 87 SiCoTHEO: Simple competitive parallel theorem provers
26. Altmetric Badge
    Chapter 88 What can we hope to achieve from automated deduction?
27. Altmetric Badge
    Chapter 89 Unification algorithms cannot be combined in polynomial time
28. Altmetric Badge
    Chapter 90 Unification and matching modulo nilpotence
29. Altmetric Badge
    Chapter 91 An improved lower bound for the elementary theories of trees
30. Altmetric Badge
    Chapter 92 INKA: The next generation
31. Altmetric Badge
    Chapter 93 XRay: A prolog technology theorem prover for default reasoning: A system description
32. Altmetric Badge
    Chapter 94 IMPS: An updated system description
33. Altmetric Badge
    Chapter 95 The tableau-based theorem prover 3T AP Version 4.0
34. Altmetric Badge
    Chapter 96 System description generating models by SEM
35. Altmetric Badge
    Chapter 97 Optimizing proof search in model elimination
36. Altmetric Badge
    Chapter 98 An abstract machine for fixed-order dynamically stratified programs
37. Altmetric Badge
    Chapter 99 Unification in pseudo-linear sort theories is decidable
38. Altmetric Badge
    Chapter 100 Theorem proving with group presentations: Examples and questions
39. Altmetric Badge
    Chapter 101 Transforming termination by self-labelling
40. Altmetric Badge
    Chapter 102 Theorem proving in cancellative abelian monoids (extended abstract)
41. Altmetric Badge
    Chapter 103 On the practical value of different definitional translations to normal form
42. Altmetric Badge
    Chapter 104 Converting non-classical matrix proofs into sequent-style systems
43. Altmetric Badge
    Chapter 105 Efficient model generation through compilation
44. Altmetric Badge
    Chapter 106 Algebra and automated deduction
45. Altmetric Badge
    Chapter 107 On Shostak's decision procedure for combinations of theories
46. Altmetric Badge
    Chapter 108 Ground resolution with group computations on semantic symmetries
47. Altmetric Badge
    Chapter 109 A new method for knowledge compilation: The achievement by cycle search
48. Altmetric Badge
    Chapter 110 Rewrite semantics for production rule systems: Theory and applications
49. Altmetric Badge
    Chapter 111 Experiments in the heuristic use of past proof experience
50. Altmetric Badge
    Chapter 112 Lemma discovery in automating induction
51. Altmetric Badge
    Chapter 113 Advanced indexing operations on substitution trees
52. Altmetric Badge
    Chapter 114 Semantic trees revisited: Some new completeness results
53. Altmetric Badge
    Chapter 115 Building decision procedures for modal logics from propositional decision procedures — The case study of modal K
54. Altmetric Badge
    Chapter 116 Resolution-based calculi for modal and temporal logics
55. Altmetric Badge
    Chapter 117 Tableaux and algorithms for Propositional Dynamic Logic with Converse
56. Altmetric Badge
    Chapter 118 Reflection of formal tactics in a deductive reflection framework
57. Altmetric Badge
    Chapter 119 Walther recursion
58. Altmetric Badge
    Chapter 120 Proof search with set variable instantiation in the Calculus of Constructions
59. Altmetric Badge
    Chapter 121 Search strategies for resolution in temporal logics
60. Altmetric Badge
    Chapter 122 Optimal axiomatizations for multiple-valued operators and quantifiers based on semi-lattices
61. Altmetric Badge
    Chapter 123 Grammar specification in categorial logics and theorem proving
62. Altmetric Badge
    Chapter 124 Path indexing for AC-theories
63. Altmetric Badge
    Chapter 125 More Church-Rosser proofs (in Isabelle/HOL)
64. Altmetric Badge
    Chapter 126 Partitioning methods for satisfiability testing on large formulas