Logic for Computer Scientists/Propositional Logic/Analytic Tableaux
Analytic Tableaux
[edit | edit source]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 | edit source]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 | edit source]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 | edit source]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.
Definition 14
[edit | edit source]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 | edit source]Give a strict tableau proof for the following formulae:
Clause Normalform Tableau
[edit | edit source]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 | edit source]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
Theorem 11
[edit | edit source]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 | edit source]A branch of a tableau for a clause set is called regular, if no literal occurs more than once.
Theorem 12
[edit | edit source]Clause normal form tableau with regularity and link condition give a decision procedure for propositional logic.
Problem (diagnosis)
[edit | edit source]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?
Footnotes
[edit | edit source]- ↑ Let be a set and a binary relation on . Then is called confluent if