In this paper the authors describe analogy-driven proof plan construction in inductive theorem proving. The analogies investigated are external analogies. An analogy procedure is obtained that is incorporated into the generic proof planner CLAM. Several examples to illustrate this procedure are presented.
Recommendations
- Reasoning by analogy in inductive logic
- An analogy principle in inductive logic
- Internal analogy in theorem proving
- scientific article; zbMATH DE number 4090850
- The problem of analogical inference in inductive logic
- Analogy in automated deduction: a survey
- Combining analogical support in pure inductive logic
- Semantic generalizations for proving and disproving conjectures by analogy
- scientific article; zbMATH DE number 1104445
- Building proofs or counterexamples by analogy in a resolution framework
Cited in
(14)- Semantic generalizations for proving and disproving conjectures by analogy
- Proof by analogy in mural
- Proving theorems by reuse
- Knowledge-based proof planning
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
- scientific article; zbMATH DE number 4164172 (Why is no real title available?)
- Formal Proof: Reconciling Correctness and Understanding
- scientific article; zbMATH DE number 4090850 (Why is no real title available?)
- scientific article; zbMATH DE number 50693 (Why is no real title available?)
- scientific article; zbMATH DE number 1104445 (Why is no real title available?)
- Internal analogy in theorem proving
- Partial matching for analogy discovery in proofs and counter-examples
- Building proofs or counterexamples by analogy in a resolution framework
- Analogy in automated deduction: a survey
This page was built for publication: Analogy in inductive theorem proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1283199)
