Change: Tableaux Algorithm

created on March 6, 2013, 3:11 p.m. by Hevok & updated on March 6, 2013, 3:14 p.m. by Hevok

Algorithms for automatic Reasoning, proof Algorithms, are able in a mechanical way, based on syntactical Rules, to proof that an Assumption or a Knowledge Base is correct or is consistent. This is a basic algorithms that one need for Reasoning.

Resolution is about a Clausal Form to begin with and than starting with this Clausal Form one tries to resolve two Clauses where one of the Variables is negated and the other is not negated, then one can resolve this two Clauses into a new Clause

In the same way as the Resolution the method of the Tableaux Algorithm is also a procedure to check the Consistency of a Logical Formula by inferring its Negation is a Contradiction. It is a proof by Refutation, completely the same as the Resolution, but it is working in a different way.

What one does in the Tableaux Algorithm is to try to construct a Decision Tree from the given Formula. In this Decision Tree each node is marked with a logical Formula. Then one has a Tree with paths and on each path from the root to the leafs, all the Formulas on the Path are Conjunctions. On the other hand, where there is branch in the path, this represents a Disjunction.

  • For automated reasoning, we need syntactic Algorithms to check the consistency of logical Assertions
  • To apply resolutions, formulas have to be in clausal form
  • The method of analytical tableaux is based on disjunctive normal form
  • Basic Idea of Tableaux Algorithm (similar to Resolution):
  • Proof algorithm (decision procedure) to check the consistency of a logical formula by inferring that its Negation is a Contradiction (proof by refutation).

One has these Paths and one tries to close this Paths. A Path is closed if along the Path as well x as not x for a Formula x occurs, where x does not have to be atomic. So one has a Formula and its Negation and along the Path from the root to the leaf, then this is closed. On the other hand if one has false in the Paths then it is also closed. The Construction of the Tree is made with the Tableaux Extension Rules. A Tableaux is fully expanded.

So one can deconstruct the entire Formula in this way. On top of this Decision Tree one has a procedure that is able to decide whether a Formula has a Contradiction or is satisfiable if no more extension Rule is applied. Then the entire Tableaux is closed if all Path of the Decision Tree have been closed. In the end a Tableaux proof for a Formula x is a closed Tableaux for not x. This means that x is True. So one tries to find a Contradiction. One tries to close the Tableaux for not x or x negated to find a Contradiction. So a closed Tableaux contains a Contradiction in this Sense.

The selection of the Tableaux Extension Rules and when to apply which one is not deterministic, but for practical use there are heuristics, especially for the Propositional Logic Tableaux to select which extension rules should be applied first to finish the Tableaux in an appropriate time.

  1. Construct a Decision Tree, where each node is marked with a logical formula.
  2. A path from the root to a leaf is the Conjunction of all formulas represented within the nodes of the path;
  3. a branch of the path represents a Disjunction.
  4. The Tree is created by successive application of the Tableaux Extension Rules.
  5. A path in the Tableaux is closed,
  6. if along the pat as well x as ¬x for a formula x occurs (x doesn't have to be atomic) or
  7. if false occurs.
  8. A tableaux is fully expanded, if no more extension Rules can be applied.
  9. A tableaux is called closed*, if all its paths are closed
  10. A Tableaux Proof for a Formula x is a closed tableaux for ¬x.

  11. The selection of the tableaux extension Rules to be applied in the Tableaux is not deterministic.

  12. There are heuristic for the Propositional Logic Tableaux to select which Rules to be applied best

For extending a Formula on can of course in the case of double negated X write X and for not true, false as well as for not False, True. To construct the entire try one has first the Conjunctive Form, the so called α-Rules and the disjunctive Formula, the so called β-Rules.

  • for PL:

      ¬¬X/X      ¬T/F     ¬F/T
    
  • for conjunctive Formula (α-Rules):

      α    X∧Y   ¬(X∨Y)  ¬(X->Y)
      --   ---   ------  -------
      α1    X      ¬X    X
      α2    Y      ¬Y    ¬Y
    
  • for disjunctive formula (β-Rules)

        β    X∨Z ¬(X∧Y) (X->Y)
      -----  --- ------ ------
      β1|β2  X|Y ∧X|∧Y  ¬X|Y
    

To proof a Formula one has first to do its Negation.

  • proof: ((q ∧ r) → (¬(q ∨ r))

    1. ¬((q ∧ r) → (¬q ∨ r))
    2. α,1: (q ∧ r)
    3. α,1: ¬(¬q ∨ r) = q ∧ ¬r
    4. α,2: q
    5. α,2: r
    6. α,3: q
    7. α,3: ¬r
  • path is closed

  • tableaux is closed

  • proof: (p → (q → r)) → ((q ∨ r)→(p → r))

    1. ¬((p → (q → r)) → ((p → q) → (p → r)))
    2. α,1: (p → (q → r))
    3. α,1: ¬((p → q) → (p → r))
    4. α,3: (p → q)
    5. α,4: ¬(p → r)
    6. α,5: p
    7. α,5: ¬r
    8. α,2: ¬p
    9. β,2: (p → r)
    10. β,9: ¬q
    11. β,9: r
    12. β,4: ¬p
    13. β,4: q

Tableaux Algorithm Extension for FOL

The Tableaux Algorithm Extension for First Order Logic works like that for Propositional Logic, but one has also to consider Formulas, Terms and Variables as well as Predicates. So one needs additional Rules, especially additional Rules for the Quantifiers.

There is the γ-Rule that applies to universal Quantified Formulas and the δ-Rule which stands for existentially quantified Formulas. Whenever there is an existential Quantifier we assume that there must exist an individual which fulfills the given Formula, therefore one can substitute x, which is a Formula with a constant that is an Individual. The same holds for negated Universal Quantifier, which is probably the same. On the hand, when considering Universal Quantification then not only for a single constant but for all possible individuals, this formula must hold. Therefore one has much more freedom, to substitute the Variable in the Formula via ground terms, which means one substitutes it with a ground term that does not occur in the originally Formula which is the only prerequisite that one has to consider.

Negation Normal Form should be preferred inside the Formula.

  • as for Propositional Logic - X and Y stand for arbitrary (FOL) Formulas
  • Additional Rules for quantified Formulas:

    γ        δ
    

    ---- ---- γ[t] δ[c]

  • γ for universally quantified formulas, δ existentially quantified Formulas, with:

       γ     γ[t]         δ     δ[c] 
     ∀x.Φ   Φ[x←t]      ∃x.Φ   Φ[x←t]
    ¬∃x.Φ  ¬Φ[x←t]     ¬∀x.Φ   ¬Φ[x←t]
    
  • t is an arbitrary ground term (i.e. does not contain variables that are bound in Φ),

  • C is a "new" constant

  • Proof: (∀x.P(x)∨Q(x)) → (∃x.P(x))∨(∀x.Q(x))

  • ¬((∀x.P(x)∨Q(x)) → (∃x.P(x))∨(∀x.Q(x)))
  • α,1 ((∀x.P(x)∨Q(x))
  • α,1 ¬((∃x.P(x))∨(∀x.Q(x))
  • α,3 ¬(∃x.P(x))
  • α,3 ¬(∀x.Q(x))
  • α,5 ¬Q(c)
  • α,4 ¬P(c)
  • α,2 ¬P(c)∨Q(c)
  • α,8 P(c) | 10. β,8 Q(c)

The Tableaux Algorithm can simply be applied to Description Logics.

lines-for-counting.png

Categories: Concept
Parent: Logic

Comment: Corrected bullet list.

See entry | Admin

Comment on This Data Unit