Proof in Tableau

Semantic tableau (plural: tableaux) is a decision/proof procedure for propositional and quantified logics.

Unsigned tableaux

mathesis.deduction.tableau.Tableau is a class for unsigned tableaux. It is initialized with an inference, given as a list of premises and of conclusions.

from mathesis.grammars import BasicGrammar
from mathesis.deduction.tableau import Tableau

grammar = BasicGrammar()

premises = grammar.parse(["A→B", "B→C"])
conclusions = grammar.parse(["A→C"])
tab = Tableau(premises, conclusions)

print(tab.htree())

A→B 1
└── B→C 2
    └── ¬(A→C) 3

A tableau is a tree of nodes, each node being a formula. Mathesis automatically indexes the nodes, so that you can access them by their index. You can apply a rule to a node of tableau with tab.apply(node, rule) where tab is a tableau:

from mathesis.grammars import BasicGrammar
from mathesis.deduction.tableau import Tableau, rules

grammar = BasicGrammar()

premises = grammar.parse(["A→B", "B→C"])
conclusions = grammar.parse(["A→C"])
tab = Tableau(premises, conclusions)

print(tab.htree())
print(f"Closed: {tab.is_closed()}\n")

tab.apply(tab[3], rules.NegatedConditionalRule())
print(tab.htree())
tab.apply(tab[1], rules.ConditionalRule())
print(tab.htree())
tab.apply(tab[2], rules.ConditionalRule())
print(tab.htree())

print(f"Closed: {tab.is_closed()}")

A→B 1
└── B→C 2
    └── ¬(A→C) 3

Closed: False

A→B 1
└── B→C 2
    └── ¬(A→C) 3
        └── A 4
            └── ¬C 5

A→B 1
└── B→C 2
    └── ¬(A→C) 3
        └── A 4
            └── ¬C 5
                ├── ¬A 6 ×
                └── B 7

A→B 1
└── B→C 2
    └── ¬(A→C) 3
        └── A 4
            └── ¬C 5
                ├── ¬A 6 ×
                └── B 7
                    ├── ¬B 8 ×
                    └── C 9 ×

Closed: True

A branch is a path from the root to a leaf of the tableau. A branch is closed if it contains a contradiction (i.e., contradictory formulas.) The tableau is closed if all branches are closed.

Signed tableaux

A signed tableau is a tableau where each node is signed with a truth value.

from mathesis.grammars import BasicGrammar
from mathesis.deduction.tableau import SignedTableau, signed_rules

grammar = BasicGrammar()

premises = grammar.parse(["A→B", "B→C"])
conclusions = grammar.parse(["A→C"])
tab = SignedTableau(premises, conclusions)

print(tab.htree())

True A→B 1
└── True B→C 2
    └── False A→C 3

First-order logic

In first-order logic, the rules extend to quantifiers as follows:

Unsigned tableaux

• NegatedParticularRule
• NegatedUniversalRule
• UniversalInstantiationRule
• ParticularInstantiationRule

from mathesis.grammars import BasicGrammar
from mathesis.deduction.tableau import Tableau, rules

grammar = BasicGrammar()

premises = grammar.parse(["P(a)", "∀x(P(x)→Q(x))"])
conclusions = grammar.parse(["Q(a)"])
tab = Tableau(premises, conclusions)

print(tab.htree())
print(f"Closed: {tab.is_closed()}\n")

tab.apply(tab[2], rules.UniversalInstantiationRule(replacing_term="a"))
print(tab.htree())

tab.apply(tab[4], rules.ConditionalRule())
print(tab.htree())

print(f"Closed: {tab.is_closed()}\n")

P(a) 1
└── ∀x(P(x)→Q(x)) 2
    └── ¬Q(a) 3

Closed: False

P(a) 1
└── ∀x(P(x)→Q(x)) 2
    └── ¬Q(a) 3
        └── P(a)→Q(a) 4

P(a) 1
└── ∀x(P(x)→Q(x)) 2
    └── ¬Q(a) 3
        └── P(a)→Q(a) 4
            ├── ¬P(a) 5 ×
            └── Q(a) 6 ×

Closed: True

Signed tableaux

WIP

Further reading

See Automated reasoning for automated reasoning with tableaux.