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).
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.
Running make
will produce the binary assn1q3
.
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:
neg
,or
andand
,imp
andiff
,
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.
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