Logic for Computer Scientists/Propositional Logic/Analytic Tableaux

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

Definition 13 edit

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:

 
  1. The tree consisting of a single node   is a tableau for   (initialisation rule).
  2. 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.

Definition 14 edit

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:

  1.  
  2.  


 

 

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

Definition 15 edit

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:


  1. The tree consisting of root   and immediate successors  , where   is a tableau for   (initialisation rule).
  2. 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:

  1. No condition.
  2. Weak link condition: There is a literal   and  .
  3. 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

 

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   of a tableau for a clause set   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:

 

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   be a set and   a binary relation on  . Then   is called confluent if