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.