[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci & Eng ] / [R J Botting] / [ MATHS ] / logic_27_Tableaux
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sat May 10 09:13:32 PDT 2008

Contents


    Semantic Tableaux

      Introduction

      Semantic tableaux are a way to find out if a set of formulas in the Lower Predicate Calculus is inconsistent. The process is quite mechanical. They may not terminate. They are not always efficient. They can need a human to supply creativity, luck, or insight. The semantic tableaux process is good for theorem proving and solving puzzles. The process always terminates on formulas in the propositional calculus. The process can be extended by rules from any theorem, algebra, or calculus that applies to the situation. Then the mechanical application of rules can go wrong and fail to prove true statements.

      The key point is that to prove that a set of premisses imply a conclusion ( if P1 and P2 and P3 and .... then Q) we start exploring the possible cases when P1, P2, P3, and (not Q) are all true. We then show that every case leads to a contradiction. The idea is to generate a set of cases that cover every possibility hidden in the initial situation. If all cases are inconsistent then so is the initial set.

      The exploration of cases is mechanical for simple propositions. It is based on the following expansions.
      FormulaCase1Case2Etc.
      P or Q ...PQ...
      not(P or Q ...)not P, not Q, ...
      P and Q ...P, Q, ...
      not(P and Q ...)not P not Q ...
      if P then Qnot PQ
      not(if P then Q)P, not Q
      P iff QP,Qnot P, not Q
      not(P iff Q)P,not Qnot P, Q
      not not PP

      These rules are pretty much equivalent to the normal propositional calculus.

      The Method of Trees

      In the standard form (suitable for board work or pen and pencil) a tree is generated. Each node has a set of formulas. This process cries out for a tool to help the user draw the tree and manage the process.

      This idea was worked out by Lewis Carrol by 1896 but his work was not published until 1977 when the drafts for Part II of "Symbolic Logic" [CarrollL77] were rediscovered, edited. and published.

      Here is a graphic cheat sheet summarizing the rules for the tree based format [ semtab.gif ] , and here are three examples: [ semtaex.jpg ] Here [ LPCtaut.gif ] is a semantic tableaux that proves a tautology in the predicate calculus

    1. (LPC)|-(for all x (F(x) and G(x))) iff (for all x(F(x)) and for all x(G(x)))

      Proof by Cases

      It is also possible to use the semantic tableaux process with my syntax for "Proof by Cases". This is suitable for presentation via the web using nested HTML tables or lists.

      Here is a proof of Modus Ponens. Given P and if P then Q show that Q must be true
      Let


      1. (let)|- (1): P,
      2. (let)|- (2): if P then Q,
      3. (let)|- (3): not Q.
      4. (2)|-
        Case
        1. not P,
        2. (1)|-RAA

        (End of Case)
        Case
        1. Q
        2. (3)|-RAA

        (Close Case )

      (Close Let )

      These proofs lend themself to being expressed using a table
      Let


      1. (let)|- (1): P,
      2. (let)|- (2): if P then Q,
      3. (let)|- (3): not Q.
      4. (2)|-
        not PQ
        (1)|-RAA(3)|-RAA

      (Close Let )

      I plan to have more examples of this -- Real soon now.

      Boolean Tableaux

      There is another way to use the idea of semantic tableaux that is suitable for work with a computer or palmtop device. Instead of drawing a tree, a formula is manipulated. Copy-and-Paste is very helpful here. The proces is very like using [ logic_25_Proofs.html#Boolean Algebra ] and is essntial "reduction to Disjunctive normal form".

      Here is a simple example of this style. Suppose we wanted to prove modus ponens: that if P implies Q and P is true then Q must also be true. We change this to checking the inconsistency of P, if P then Q, and not Q. Here I use The notation of Boolean algebra.

      Prove P and (if P then Q) and not Q are inconsistent.
      Consider


        P * (if P then Q) * -Q.
      1. = P * ( -P+ Q) * -Q.
      2. = P * -P * -Q + P * Q * -Q.
      3. = 0 + 0
      4. = 0

      (Close Consider )

      In this form of derivation I'd suggest using these notations for semantic tableaux.
      P,Q,R,...well formed formulas
      P[t/x] replace all free variable x by a term t where no free variable in t is bound in P.
      n,m numbers like 2,3,4,....
      and, or, not, iff, if_thenMATHS operators
      for all, for some, for no,....quantifiers.
      *Shorthand form for and from Boolean Algebra.
      +Shorthand form for or from Boolean Algebra.
      0Shorthand for false - closing an alternative

      Start a semantic tableaux by assuming all the premises aand the negation of the consequence. To attempt to prove a sequent P,Q,...,R|-S start with

    2. P * Q * ...*R -(S). or in graphic form
      1. P
      2. Q
      3. ...
      4. R
      5. not(S)

      If the semantic tableaux terminates then either all possibilities are inconsistent and the result is proved, or a set of counter examples has been generated. Sometimes the process does not terminate without some luck or inspiration.

      Here is the semantic tableaux process. Firstly: use boolean algebra to maintain a disjunctive normal form where the possibilities are ored together. Use distributive and assorbative laws for embedded ors:

    3. embedded_or::=following,
      Net

      1. |- (absorb): (P + Q) * Q = Q.
      2. |- (resolve): P * (-P+Q) = P*Q.
      3. |- (distribute1): (P+Q) * R = P*R + Q*R.
      4. |- (distribute2): (P+Q)*(R+S) = P*R + Q*R + P*S + Q*S.

      (End of Net)

      Use commutative laws to reorder the sub-formula.

      Second, remove all conjunctions that have a formula P and its negation -P. Remove conjunctions with false parts like (not x=x).

      Pick a sub-formula and match it to the the table below. Check the conditions and apply the step. Mostly replace one formula by others. Sometimes the first formula is kept.
      GivenConditionsAddRemove it?
      -- P-PYes
      -(P+Q)-- P * - QYes
      -(if P then Q)-P * - QYes
      if P then Q-- P+ QYes
      P+Q-embedded_ors aboveYes
      P iff Q-(P *Q + - P * - Q)Yes
      -(P iff Q)-(P * - Q + - P * Q)Yes
      for some x(P)v is some unused variableP[v/x]Yes
      - for all x(P)v is some unused variable- P[v/x]Yes
      for one x(P)v is some unused variableP[v/x] and for all x( if P then x=v)Yes
      for n x(P)n>1, v is some unused variable, m=n-1P[v/x], for m x( P and x<>v)Yes
      for all x(P)t is ANY termP[t/x]No
      - for some x(P)t is ANY term- P[t/x]No
      for no x(P)t is ANY term- P[t/x]No
      - for one x(P)y is free for x in Pfor no x(P) + for some x,y(x<>y and P and P[y/x]No

      You can split each alternative into a separate analysis if you need.

      Example 2


      for some x(F(x)), for all x(if F(x) then G(x))|-for some x(G(x))
      Consider
      1. for some x(F(x)) * for all x( if F(x) then G(x)) * - for some x(G(x)).
      2. F(a)* for all x(if F(x) then G(x))* - for some x(G(x)).
      3. F(a)* if F(a) then G(a)* for all x(if F(x) then G(x))* - for some x(G(x)).
      4. F(a)* (- F(a)+ G(a))* for all x(if F(x) then G(x))* - for some x(G(x)).
      5. F(a)* G(a)* for all x(if F(x) then G(x))* - for some x(G(x)).
      6. F(a)* G(a)* not G(a)* for all x(if F(x) then G(x))* - for some x(G(x)).
      7. 0

      (Close Consider )

      Bad News

      The above rules allow choices. Choices imply non-determinism, intuition, experience, luck, etc. all play a part. In other words you may try a lot of wrong choices before getting the right way to tackle the problem.

      Non-termination comes from not deleting some formulas.

      The rules can grow large expressions. This is a symptom of is a known intractable problem.

      More on Semantic Tableaux

        Online

        [ index.html ] (PC limitted interactive tool)

        [ index.pl?node_id=1513374 ] (brief description and theory)

        [ http://www.umsu.de/logik/trees/ ] (tool inputs a formula checks it for validity and generatest a semantic tableaux)

        Hodges77

        1. Wilfrid Hodges
        2. Logic
        3. Penguin Books Middlesex UK & NY NY 1977
        4. =TEXT FORMAL LOGIC Semantic Tableaux TREEs
        5. Describes an easy to learn and use method of proving/disproving results.
        6. Compare with earlier

        Jeffrey91

        1. Richard C Jeffrey (Princeton U)
        2. Formal Logic: Its Scope and Limits
        3. McGraw-Hill Higher Education NY NY 1991 ISBN 0-07-032357-7
        4. =TEXT FORMAL LOGIC semantic Tableaux TREES
        5. Previous edition was in 1960s.
        6. An easy to use way of proving things.
        7. Compare with the earlier Hodges77 above.

        Smullran95

        1. Raymond M. Smullyan
        2. First-Order Logic
        3. Dover Publications (1995) ISBN: 0486683702 QA9.S57
        4. Springer-Verlag, 1968

      Note

      Semantic Tableaux proofs tend to be almost mechanical except for (1) choosing an expression to substitute for universally quantified variables (2) selecting the special cases to analyze. This can be quite difficult. Much theoretical work has been done in the field of Artificial Intelligence to make this as automatic as possible. It has been shown that in any interesting logic there can not exist an algorithm that will prove all true statements.

    . . . . . . . . . ( end of section Semantic Tableaux) <<Contents | End>>

    Notes on MATHS Notation

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

    For a complete listing of pages in this part of my site by topic see [ home.html ]

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

    Glossary

  2. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

End