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 non-branching 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 alpha-rule 4:  [[b, a, ~c, a->(b->c)]] 
By beta-rule 2:   [[b, a, ~c, ~a], [b, a, ~c, b->c]] 
A branch closed:  [[b, a, ~c, b->c]] 
By beta-rule 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 beta-rule 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. First-Order Logic. Springer-Verlag: 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. 101-178. Elsevier, 2001. 
Available from http://www.cs.chalmers.se/~reiner/pub.html.