PROJECT 2.
IMPLEMENTATION OF SEMANTIC TABLEAUX PROOF PROCEDURE FOR PROPOSITIONAL LOGIC
===========================================================================
1. Propositional Semantic Tableaux
Propositional semantic tableaux is one of the proof procedures for propositional logic.
It is a refutation system: to prove a formula F we begin with not(F) and produce a contradiction.
The procedure for doing this involves expanding not(F). In tableaux proofs, such an expansion
takes the form of of a tree, where nodes are labeled with formulas. Each branch of the
tree should be thought of as representing the conjunction of the formulas appearing on it,
and the tree itself as representing the disjunction of its branches.
The propositional semantic tableaux procedure consists of nine inference rules
(called tableaux expansion rules) groupped into so called Alpha and Beta rules:

Alpha rules
1. not(not(A))


F
2. A and B


A,B
3. not(A or B)


not(A),not(B)
4. not(A implies B)


A,not(B)

Beta rules
1. A or B
/ \
/ \
A B
2. A implies B
/ \
/ \
not(A) B
3. not( A and B)
/ \
/ \
not(A) not(B)
4. A equivalent B
/ \
/ \
A,B not(A),not(B)
5. not(A equivalent B)
/ \
/ \
not(A),B A,not(B)

Given a set of assumptions S and a goal G, Repeated application of these rules
generates a proof tree with the set S union {not(G)} at the root. A branch of
this proof tree can be "closed" if a sentence and its negation both occur on
the branch. The process terminates in success if all branches can be closed
in this way. It terminates in failure if at least one branch fails to close
with no more inference rules applicable on that branch.
==================================================
2. Requirements.
Write a Prolog program that implements the propositional semantic tableaux
proof procedure. The program
1. Accepts a set of propositional formulas (the assumptions) and a
propositional formula (the goal) as an input.
2. Builds the semantic tableaux tree for the assumptions and the
negated goal (heuristics: apply nonbranching rules first. Usually
this will result in shorter proofs).
3. Represents the tree as a list of branches, and each
branch as a list of logical formulas. When a tableaux expansion rule
is applied to a formula on a branch, the list representing that branch
becomes transformed into either one or two new branches. When a branch
is closed, the corresponding list is eliminated. Thus, if all the branches
can be closed, the resulting tree is represented by the empty list
(i.e. a tree without branches).
4. Produces an output a proof trace: rules applied and their result.
Examples are provided below.
5. Should have options to choose between taking the input either from
the keyboard, or from a file. The output also optionally should be
shown on the screen or written to a file.
6. Uses operator declarations.
7. Is well documented.
Examples:
? prove(b>(a>c), [a>(b>c)]).
Initial: [[~(b>(a>c), a>(b>c)]]
By alpha rule 4: [[b, ~(a>c), a>(b>c)]]
By alpharule 4: [[b, a, ~c, a>(b>c)]]
By betarule 2: [[b, a, ~c, ~a], [b, a, ~c, b>c]]
A branch closed: [[b, a, ~c, b>c]]
By betarule 2: [[b, a, ~c, ~b], [b, a, ~c, c]]
A branch closed: [[b, a, ~c, c]]
A branch closed: []
The proof succeeds.
Yes
?prove(p, [p v ~p])
Initial: [[~p, p v ~p]]
By betarule 1: [[~p, p], [~p, ~p]]
A branch closed: [[~p, ~p]]
There is a branch on which closure fails: [[~p,~p]]
The proof fails.
No
=========================================================
3. References.
1. R. M. Smullyan. FirstOrder Logic. SpringerVerlag: Heidelberg, Germany, 1968.
2. R. Haehnle. Tableaux and Related Methods. In: A. Robinson and A. Voronkov
(eds), Handbook of Automated Reasoning. V.1, Chapter 3, pp. 101178. Elsevier, 2001.
Available from http://www.cs.chalmers.se/~reiner/pub.html.