Logic for Computer Scientists/Propositional Logic/Analytic Tableaux

From Wikibooks, open books for an open world
< Logic for Computer Scientists‎ | Propositional Logic
Jump to: navigation, search

Analytic Tableaux[edit]

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[edit]

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[edit]

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[edit]

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 inT. 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:

Table1Correspondance between.png
  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).
Table2Correspondance.png

One tableau for our example is depicted in figure 2.

Definition 14[edit]

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)[edit]

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

Figure2Atableaufora.png

Clause Normalform Tableau[edit]

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[edit]

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).
Figure3tableau.png


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

Tableau1.png


and finally a model elimination tableau is given by

Tableau2.png

Theorem 11[edit]

Clause normal form tableau are complete.
Note that strong link condition do not allow for confluent [1]

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[edit]

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

Theorem 12[edit]

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

Problem (diagnosis)[edit]

Consider this electronic circuit with two input lines and one output line:

Image-Inv-inv.png

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?

Footnotes[edit]

  1. Let M be a set and \to a binary relation on M. Then (M, \to) is called confluent if 
\text{for all }  u,v,x,y \; \text{ and }  \; u \stackrel{*}{\to} x \; \text{ and } \; u \; \stackrel{*}{\to} \; y \;\; \text{ there is a } \; z \; \text{ with } \; x
\stackrel{*}{\to} \; z \;  \text{ and }  y \; \stackrel{*}{\to}\; z