Related Experiment Videos
A precondition prover for analogy
1Department of Computer Science, University of Texas at Austin 78712, USA.
Bio Systems
|January 1, 1995
Summary
A new theorem prover, PC, generates a precondition when unable to prove a formula, enabling proofs by analogy. This automated proof-plan debugging facilitates proving similar theorems, demonstrating its utility in automated reasoning.
Area of Science:
- Automated Reasoning
- Mathematical Logic
Background:
- Theorem provers typically succeed or fail to prove a given formula.
- Proof by analogy is a challenging area in automated theorem proving.
Purpose of the Study:
- Introduce a novel theorem prover, PC, capable of generating preconditions.
- Demonstrate the application of PC for automated proofs by analogy.
- Explore the debugging of proof-plans for analogous theorem proving.
Main Methods:
- The PC prover returns a precondition Q such that (Q-->F) is provable when F cannot be directly proved.
- Utilizes proof-plans, initially employing abduction in the absence of a plan.
- Applies a guiding proof's plan to construct and debug proofs for similar theorems.
Main Results:
- Successfully demonstrated proofs by analogy for simple example theorems.
- Showcased automated proof-plan debugging for a difficult theorem pair (Ex4 and Ex4L).
- Extended the methodology to address complex resolution theory theorems (GCR and GCLR), though not fully completed.
Conclusions:
- The PC prover effectively supports proofs by analogy through automated proof-plan debugging.
- The system shows promise for tackling complex theorems in mathematical logic and automated reasoning.
- Further development is needed to fully handle intricate theorems like GCR and GCLR.