Logic for Computer Scientists/Propositional Logic/Analytic Tableaux

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 History

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.

The Calculus

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 $\{\lnot P\land \lnot (Q\lor R),\lnot (Q\land \lnot R)\}$ . 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: $\alpha$ for formulas of conjunctive type, $\beta$ for formulas of disjunctive type in the propositional case. Note that in the above example $\lnot (Q\land \lnot R)$ 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 $\alpha$ and $\beta$ 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.

Definition 13

A tableau for a logic $L$ is a finitely branching tree whose nodes are formulas from $L$. A branch in a tableau $T$ is a maximal path in$T$. When no confusion can arise, branches are frequently identified with the set of their nodes (formulas). Given a set $\Phi$ of formulae from $L$, a tableau for $\Phi$ is constructed by a (possibly infinite) sequence of applications of the following rules:

1. The tree consisting of a single node $true$ is a tableau for $\Phi$ (initialisation rule).
2. Let $T$ be a tableau for $\Phi$, $B$ a branch of $T$, and $\psi$ a formula in $B\cup \Phi$. If the tree $T'$ is constructed by extending $B$ by as many new linear subtrees as an instance of a tableau rule schema in Table 2 with premise $\psi$ has extensions, and the nodes of the new subtrees are the formulas in the extensions of the rule instance, then $T'$ is a tableau for $\Phi$ (expansion rule).

One tableau for our example is depicted in figure 2.

Definition 14

In a tableau $T$ for a set $\Phi$ of sentences a branch $B$ is closed iff $B\cup \Phi$ contains a pair $\phi ,\lnot \phi$ of complementary formulas, or $false$; otherwise, it is open. A tableau is closed if all its branches are closed. A tableau proof for (the unsatisfiability of) a set $\Phi$ of formulae is a closed tableau $T$ for $\Phi$.

Problem 31 (Propositional)

Give a strict tableau proof for the following formulae:

1. $\lnot ((A\downarrow B)\downarrow (A\lor B))$
2. $((A\to B)\land (B\to C))\to (\lnot (\lnot C\land A))$

$\Box$

Clause Normalform Tableau

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 $\lor$-junctors. Hence every clause is of $\beta$-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 $\beta$-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 $\beta$-rule-applications with clauses from S can be used. Which of the clauses is allowed is controlled by a link condition.

Definition 15

A clause (normalform) tableau for a set of clauses $S$ is a tableau for $S$, whose nodes are literals from $S$ and which is constructed by a (possibly infinite) sequence of applications of the following rules:

1. The tree consisting of root $true$ and immediate successors $L_{1},\cdots ,L_{n}$, where $C=L_{1},\cdots ,L_{n}\in S$ is a tableau for $S$ (initialisation rule).
2. Let $T$ be a tableau for $S$, $B$ a branch of $T$, and $C=L_{1},\cdots ,L_{n}\in S$, such that the link-condition (see below) is satisfied. If the tree $T'$ is constructed by extending $B$ by the $n$ subtrees $L_{i}$, then $T'$ is a tableau for $S$ (expansion rule).

The following are three possible link conditions:

1. No condition.
2. Weak link condition: There is a literal $L\in B$ and ${\overline {L}}\in C$.
3. Strong link condition: Let $L$ be the leaf of $B$, then there is ${\overline {L}}\in C$.

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

Theorem 11

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:

Definition 16

A branch $B$ of a tableau for a clause set $S$ is called regular, if no literal occurs more than once.

Theorem 12

Clause normal form tableau with regularity and link condition give a decision procedure for propositional logic.

Problem (diagnosis)

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".

1. 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).
2. 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?
3. 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?
4. 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?