Skip to main content

Questions tagged [tableau]

Use this tag with tableau method. In proof theory, the semantic tableau (also called truth tree) is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. (from Wikipedia)

Filter by
Sorted by
Tagged with
4 votes
1 answer
146 views

Tutorial implementation of analytic tableaux

I am re-reading John Harrison's wonderful Handbook of Practical Logic and Automated Reasoning, and he has a rather idiosyncratic presentation of analytic tableaux. What other tutorial implementations ...
Alex Nelson's user avatar
  • 1,564
16 votes
2 answers
194 views

Are there any proof assistants or theorem provers based on the method of analytic tableaux?

Are there any proof assistants or theorem provers based on the method of analytic tableaux? A closed tableau makes the branching structure of a proof using case analysis very obvious. I like tableau ...
Greg Nisbet's user avatar
  • 2,761