Exercise 7: A simple FOL prover

Overview

Play with a backwards prover implementing FOL in LK. This prover uses explicit terms for all on the left and exists on the right.

Code is in Code/FOL

Key files: Examples, LK

Alternate resource: Check out Larry Paulson's FOL theorem prover linked from this page: http://www.cl.cam.ac.uk/teaching/1011/LogicProof/

Fire up ghci; load FOL/Examples.hs

We prove example formula "m3" as follows:

*Examples> proveM (SequentM [] [m3]) []
|- ((ALL a. O(a, a)) --> (ALL a. (EX b. O(a, b))))

As in the other backwards provers, the list is a list of rules. We begin with implies on the right:

*Examples> proveM (SequentM [] [m3]) [iR]
(ALL a. O(a, a)) |- (ALL a. (EX b. O(a, b)))

We continue with all on the right, which introduces a new variable ?b, that is fresh:

*Examples> proveM (SequentM [] [m3]) [iR,alR]
(ALL a. O(a, a)) |- (EX b. O(?b, b)), (ALL a. (EX b. O(a, b)))

Next we apply exists on the right, providing a term as required by the rule:

*Examples> proveM (SequentM [] [m3]) [iR,alR,eR (toTerm "?b")]
(ALL a. O(a, a)) |- O(?b, ?b), (ALL a. (EX b. O(a, b)))

This is followed with all on the left, which also requires a term. We again use "?b" as the term:

*Examples> proveM (SequentM [] [m3]) [iR,alR,eR (toTerm "?b"), alL (toTerm "?b")]
O(?b, ?b) |- O(?b, ?b), (ALL a. (EX b. O(a, b)))

We complete the proof with the axiom rule:

*Examples> proveM (SequentM [] [m3]) [iR,alR,eR (toTerm "?b"),alL (toTerm "?b"),ax]

*Examples>

The proof succeeds silently.