Proving theorems by reuse

DOI10.1016/S0004-3702(99)00096-XzbMATH Open0939.68823OpenAlexW2117752042MaRDI QIDQ1978233FDOQ1978233

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

zbMATH Keywords

machine learningabstractionknowledge representationanalogydeduction and theorem provingreuseproblem solving and search

Mathematics Subject Classification ID

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Analogy in inductive theorem proving
• Proving theorems by reuse
• Productive use of failure in inductive proof
• Learning by understanding analogies
• Automatically generating abstractions for planning
• On proving the termination of algorithms by machine
• A theory of abstraction
• Learning domain knowledge to improve theorem proving
• Lazy generation of induction hypotheses
• Proving and applying program transformations expressed with second-order patterns
• Rippling: A heuristic for guiding inductive proofs
• A unification algorithm for typed \(\overline\lambda\)-calculus
• The undecidability of the second-order unification problem
• Explanation-based generalisation \(=\) partial evaluation
• The OYSTER-CLAM system
• Theorem proving with abstraction
• A paradigm for reasoning by analogy
• Computational approaches to analogical reasoning: A comparative analysis
• Semantic generalizations for proving and disproving conjectures by analogy
• Coloring terms to control equational reasoning
• Reuse of proofs in software verification
• Experiments in the heuristic use of past proof experience
• Lemma discovery in automating induction
• On terminating lemma speculations.
• INKA: The next generation
• Plagiator — A learning prover
• Partial matching for analogy discovery in proofs and counter-examples

Cited In (6)

• On terminating lemma speculations.
• Termination of theorem proving by reuse
• Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
• Deduction as an Engineering Science
• Analogy in Automated Deduction: A Survey
• Proving theorems by reuse

Uses Software

• PLAGIATOR
• NQTHM
• SPIKE
• InKa
• DISCOUNT
• CLAM
• Oyster
• Prodigy
• RRL

This page was built for publication: Proving theorems by reuse

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1978233)