SequentProver

A simple implementation of a theorem prover using sequent calculus with some supplied rules (as part of an assignment for a knowledge representation and reasoning course at UNSW).

Basics

Below, , , , and are (possibly empty) strings of formulae, and and are non-empty formulae. The following 11 rules are those which the prover uses to construct its proof:

To do so, it searches backwards, starting with the sequent to prove. For example, one possible proof that is

Instead of searching forward for a proof, we can begin at , and apply rules P4a, P2a, and P5b backwards, where P5b splits up into two sequents, and , which can both be proven by P1.

Usage

Running make will produce the binary assn1q3.

Input

The program is run as ./assn1q3 <sequent>, where <sequent> is of the form [formulae] seq [formulae]. The formulae consist of comma-separated formulae using the following representations:

Symbol	Representation	Description
	neg	Negation
	or	Disjunction
	and	Conjunction
	imp	Implication
	iff	Bi-implication

Any other input is treated as an atom (for example, hello), which is case-sensitive. Grouping is by parentheses (), and order of precedence is right associative, in the order:

1. neg,
2. or and and,
3. imp and iff,

So, neg p or q and r or s imp t is parsed as ((neg p) or (q and (r or s))) imp t.

The sequent could be input as [phi, (phi imp psi) and rho] seq [psi or neg rho].

Theorems can be inputted by leaving the left side of the sequent empty, so [] seq [p or neg p], for example.

Output

The first line of output (assuming valid input) will be either true or false, indicating whether a proof of the sequent was found. If it is true, then the proof found will be output on the following lines. For example:

$ ./assn1q3 `[p imp q, q] seq [p]`
false
$ ./assn1q3 `[p imp q] seq [q or neg p]`
true
1: [q] seq [q, neg p] ... via P1
2: [q] seq [q or (neg p)] ... via P4a from 1
3: [p] seq [q, p] ... via P1
4: [] seq [q, neg p, p] ... via P2a from 3
5: [] seq [q or (neg p), p] ... via P4a from 4
6: [p imp q] seq [q or (neg p)] ... via P5b from 2, 5