Proving theorems by reuse
From MaRDI portal
Publication:1978233
DOI10.1016/S0004-3702(99)00096-XzbMath0939.68823OpenAlexW2117752042MaRDI QIDQ1978233
Christoph Walther, Thomas Kolbe
Publication date: 4 June 2000
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0004-3702(99)00096-x
knowledge representationabstractionmachine learningreuseanalogydeduction and theorem provingproblem solving and search
Related Items
Proof generalization in \(\mathrm {LK}\) by second order unifier minimization ⋮ Proving theorems by reuse ⋮ Deduction as an Engineering Science ⋮ Analogy in Automated Deduction: A Survey ⋮ On terminating lemma speculations.
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Rippling: A heuristic for guiding inductive proofs
- Learning by understanding analogies
- Explanation-based generalisation \(=\) partial evaluation
- Computational approaches to analogical reasoning: A comparative analysis
- Theorem proving with abstraction
- The undecidability of the second-order unification problem
- A theory of abstraction
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Proving and applying program transformations expressed with second-order patterns
- Analogy in inductive theorem proving
- Automatically generating abstractions for planning
- On proving the termination of algorithms by machine
- Coloring terms to control equational reasoning
- Semantic generalizations for proving and disproving conjectures by analogy
- Reuse of proofs in software verification
- On terminating lemma speculations.
- Productive use of failure in inductive proof
- Proving theorems by reuse
- A paradigm for reasoning by analogy
- Learning domain knowledge to improve theorem proving
- INKA: The next generation
- Experiments in the heuristic use of past proof experience
- Lemma discovery in automating induction
- Lazy generation of induction hypotheses
- Plagiator — A learning prover
- Partial matching for analogy discovery in proofs and counter-examples
