structure for 'Theory of Logic'    |     alphabetical list of themes    |     expand these ideas

5. Theory of Logic / H. Proof Systems / 5. Tableau Proof

[proof by eliminating branches on inference trees]

8 ideas
Tableau proofs use reduction - seeking an impossible consequence from an assumption [Bostock]
Non-branching rules add lines, and branching rules need a split; a branch with a contradiction is 'closed' [Bostock]
A completed open branch gives an interpretation which verifies those formulae [Bostock]
A tree proof becomes too broad if its only rule is Modus Ponens [Bostock]
Unlike natural deduction, semantic tableaux have recipes for proving things [Bostock]
In a tableau proof no sequence is established until the final branch is closed; hypotheses are explored [Bostock]
Tableau rules are all elimination rules, gradually shortening formulae [Bostock]
If an argument is invalid, a truth tree will indicate a counter-example [Girle]