Proving theorems by reuse
From MaRDI portal
Publication:1978233
machine learningabstractionknowledge representationanalogydeduction and theorem provingreuseproblem solving and search
Recommendations
Cites work
- scientific article; zbMATH DE number 4051039 (Why is no real title available?)
- scientific article; zbMATH DE number 4072439 (Why is no real title available?)
- scientific article; zbMATH DE number 4090850 (Why is no real title available?)
- scientific article; zbMATH DE number 4112064 (Why is no real title available?)
- scientific article; zbMATH DE number 3702108 (Why is no real title available?)
- scientific article; zbMATH DE number 43237 (Why is no real title available?)
- scientific article; zbMATH DE number 52140 (Why is no real title available?)
- scientific article; zbMATH DE number 3467028 (Why is no real title available?)
- scientific article; zbMATH DE number 1324439 (Why is no real title available?)
- scientific article; zbMATH DE number 1324445 (Why is no real title available?)
- scientific article; zbMATH DE number 592370 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1552515 (Why is no real title available?)
- A paradigm for reasoning by analogy
- A theory of abstraction
- A unification algorithm for typed -calculus
- Analogy in inductive theorem proving
- Automatically generating abstractions for planning
- Coloring terms to control equational reasoning
- Computational approaches to analogical reasoning: A comparative analysis
- Experiments in the heuristic use of past proof experience
- Explanation-based generalisation \(=\) partial evaluation
- INKA: The next generation
- Lazy generation of induction hypotheses
- Learning by understanding analogies
- Learning domain knowledge to improve theorem proving
- Lemma discovery in automating induction
- On proving the termination of algorithms by machine
- On terminating lemma speculations.
- Partial matching for analogy discovery in proofs and counter-examples
- Plagiator — A learning prover
- Productive use of failure in inductive proof
- Proving and applying program transformations expressed with second-order patterns
- Proving theorems by reuse
- Reuse of proofs in software verification
- Rippling: A heuristic for guiding inductive proofs
- Semantic generalizations for proving and disproving conjectures by analogy
- The OYSTER-CLAM system
- The undecidability of the second-order unification problem
- Theorem proving with abstraction
Cited in
(14)- On terminating lemma speculations.
- Algebraic Methodology and Software Technology
- A pragmatic approach to reuse in tactical theorem proving
- Analogy in automated deduction: a survey
- Reuse of proofs in software verification
- Deduction as an engineering science
- What's in a theorem name?
- Termination of theorem proving by reuse
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
- Boosting the reuse of formal specifications
- Enhanced Theorem Reuse by Partial Theory Inclusions
- Theorem Proving in Higher Order Logics
- scientific article; zbMATH DE number 1552515 (Why is no real title available?)
- Proving theorems by reuse
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)
