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.

Getting Started

Code is in Code/FOL

Key files: Examples, LK

A short demo:

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.

What to do

1. Work some examples from HR Exercises 2.3 problems 9 and 13.