Logic for Computer Scientists/Propositional Logic/Analytic Tableaux
In this section we present a calculus, namely analytic tableau, which is an alternative to resolution. Although this calculus was developed independently from resolution, it will turn out that there are some interesting common features. The most obvious difference is, that analytic tableau work direct on formulae, there is no need to transform a formulae in a clausal normal form.
Tableaux - A Short HistoryEdit
The development of tableaux calculi started in the 1950th. The first authors to be mentioned are Beth (1955), Hintikka (1955) and Schütte (1956). Their goal was primarily to develop calculi without meta-language constructs. Later in the 1960th the idea of derivation trees and nodes in such a tree labeled by formulae became famous as the concept of analytic tableaux introduced by Smullyan 1968. The idea of mechanisation of tableaux calculi was then introduced by Kanger 1957, Prawitz 1960, Wang 1960, Davis 1960 and Maslov 1968.
Later on the concept of analytic tableaux was modified and refined for its use in automated deduction by Loveland 1968 (Model elimination), Kowalski, Kuehner 1971 (SL-resolution) and Bibel 1975, Andrews 1976 (Connection or matings methods). Nowadays there are numerous high performance theorem provers based on this work.
One of the advantages of tableaux calculi is that can be defined
without transforming the formula into clause normal form.
Example Given a set of formulae . We are aiming at constructing a tree, whose branches contain nodes which are labeled with formulae.
For this it is important to analyse the formula according to its leading connective. Smullyan observed that some work can be saved if non-literal formulas are grouped into types which are treated identically: for formulas of conjunctive type, for formulas of disjunctive type in the propositional case. Note that in the above example has to be treated as a formula of disjunctive type, because of the negation standing in front of the conjunction. Correspondence between formulas and their types is summarised in Table 1. The letters and are used to denote formulas of (and only of) the appropriate type. Let us now define the basic data structure for tableaux calculi together with the corresponding extension rules.
A tableau for a logic is a finitely branching tree whose nodes are formulas from . A branch in a tableau is a maximal path in . When no confusion can arise, branches are frequently identified with the set of their nodes (formulas). Given a set of formulae from , a tableau for is constructed by a (possibly infinite) sequence of applications of the following rules:
- The tree consisting of a single node is a tableau for (initialisation rule).
- Let be a tableau for , a branch of , and a formula in . If the tree is constructed by extending by as many new linear subtrees as an instance of a tableau rule schema in Table 2 with premise has extensions, and the nodes of the new subtrees are the formulas in the extensions of the rule instance, then is a tableau for (expansion rule).
One tableau for our example is depicted in figure 2.
In a tableau for a set of sentences a branch is closed iff contains a pair of complementary formulas, or ; otherwise, it is open. A tableau is closed if all its branches are closed. A tableau proof for (the unsatisfiability of) a set of formulae is a closed tableau for .
Problem 31 (Propositional)Edit
Give a strict tableau proof for the following formulae:
Clause Normalform TableauEdit
Let us now refine the calculus for the special case, that we deal with sets of clauses, which represent a formula in CNF. Note that in the case of conjunctive normal form clauses we only have literals, which are connected by -junctors. Hence every clause is of -type. In figure 3 a tableau for a set of clauses is given. The clauses from the given clause set form the initial tableau; then there is only the -rule applicable for further extensions of the tableau.
In the following formal definition of a clause normal form tableau we start with an initial tableau, which is formed by taking an arbitrary clause from the given clause set S. For further extensions of the tableau -rule-applications with clauses from S can be used. Which of the clauses is allowed is controlled by a link condition.
A clause (normalform) tableau for a set of clauses is a tableau for , whose nodes are literals from and which is constructed by a (possibly infinite) sequence of applications of the following rules:
- The tree consisting of root and immediate successors , where is a tableau for (initialisation rule).
- Let be a tableau for , a branch of , and , such that the link-condition (see below) is satisfied. If the tree is constructed by extending by the subtrees , then is a tableau for (expansion rule).
The following are three possible link conditions:
- No condition.
- Weak link condition: There is a literal and .
- Strong link condition: Let be the leaf of , then there is .
In fact we have defined three different calculi:
- Without link condition it is called clause normal form tableau,
- with the weak link condition we call it connection calculus, and
- with the strong link condition it is called model elimination.
An example for clause normal form tableau was given in figure 3. An example for a connection calculus tableau is
and finally a model elimination tableau is given by
Clause normal form tableau are complete.
Note that strong link condition do not allow for confluent 
proof procedures. If no link condition (i.e. the empty one) is applied it is trivial to get a confluent version. For the case of weak link condition this is not obvious. In order to arrive at a decision procedure for propositional clauses we need an extra condition:
A branch of a tableau for a clause set is called regular, if no literal occurs more then once.
Clause normal form tableau with regularity and link condition give a decision procedure for propositional logic.
Consider this electronic circuit with two input lines and one output line:
Suppose, as depicted, that both input lines are "1" and that the output line is "1", thus contradicting the expected output value "0".
- First, formalize the circuit, i.e. the functionality of the three components and the two connections by neglecting the possibility of not correctly functioning components (i.e. do not use abnormal -Literals).
- Consider the value pairs "0-0", "1-0" and "1-1" to be supplied to the input lines. For each of these, using the result from (1) compute the expected output value by means of analytic tableau. How did you read off the results from the tableaux?
- Use your formalization and analytic tableau to prove that the output value "1" contradicts the expected behavior in case of input "1-1". How did you read off the result from the tableau?
- Now modify the formalization of the components in (1) by abnormal -literals as shown in class. Use analytic tableau to compute all possible diagnosis for the input "1-1" and output "1". How did you read off the result from the tableau?
- Let be a set and a binary relation on . Then is called confluent if