# Exercise 5: A simple FOL, Sequent Based, 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 here.

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/LK.hs

We prove example formula **(forall x. P(x)) --> (forall y. P(F(y)))** as follows:

m1 = (replayM s1 [impliesR 1, allR 1, allL (toTerm "F(?b)") 1, axiom 1 1])

As in the other backwards provers, the list is a list of rules. We begin with implies on the right **(impliesR 1)**:
This turns the sequent with only an implication

|- ((ALL x. P(x)) --> (ALL y. P(F(y))))

into one with terms on both sides of the turnstile.
(ALL x. P(x)) |- (ALL y. P(F(y)))

We continue with all on the right **(allR 1)**, which introduces a new variable ?b, that is fresh:

(ALL x. P(x)) |- P(F(?b)), (ALL y. P(F(y)))

Note how it also duplicates the for all, a specialized instance (with the fresh varaibale) and the old quantified instance.
Next we apply exists on the right, providing a term as required by the rule:

P(F(?b)) |- P(F(?b)), (ALL y. P(F(y)))

This is followed with all on the left **(allL (toTerm "F(?b)") 1)**,
which also requires a term. We choose "F(?b)" .

We complete the proof with the axiom rule **(axiom 1 1)**, which leaves us with:

QED

## What to do

- Work some examples (at least 3). You can find some in Smullyan or in Coble, or make up your own.
- Study the rules al,ar,ol,ar,il,ir, etc. (lines 198-225) that add some search.
- convince your self that they will work
- then redo at least 2 of your examples.

## What to turn in.

- Create a file (that imports LK.hs) with your examples, and submit it to D2l
- Be prepared to talk about your solution in class.

Back to the class web-page.