# 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.

## Learning Objectives

## Getting Started

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/

## A short demo:

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.

## What to do

- Work some examples from HR Exercises 2.3 problems 9 and 13.
- Advanced: Add some automation? Play with Paulson's prover.

## What to turn in.

- Create a named subfolder of Ex7 with your examples
- Be prepared to talk about your solution in class.

Back to the class web-page.

Back to the Course Schedule.