A precondition prover for analogy.

We describe here a prover PC (precondition) that normally acts as an ordinary theorem prover, but which returns a 'precondition' when it is unable to prove the given formula. If F is the formula attempted to be proved and PC returns the precondition Q, then (Q-->F) is a theorem (that PC can prove). This prover, PC, uses a proof-plan. In its simplest mode, when there is no proof-plan, it acts like ordinary abduction. We show here how this method can be used to derive certain proofs by analogy. To do this, it uses a proof-plan from a given guiding proof to help construct the proof of a similar theorem, by 'debugging' (automatically) that proof-plan. We show here the analogy proofs of a few simple example theorems and one hard pair, Ex4 and Ex4L. The given proof-plan for Ex4 is used by the system to prove automatically Ex4; and that same proof-plan is then used to prove Ex4L, during which the proof-plan is 'debugged' (automatically). These two examples are similar to two other, more difficult, theorems from the theory of resolution, namely GCR (the ground completeness of resolution) and GCLR (the ground completeness of lock resolution). GCR and GCLR have also been handled, in essence, by this system but not completed in all their details.