O'Reilly logo

Handbook of Practical Logic and Automated Reasoning by John Harrison

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

Tableaux

Although the prawitz procedure is usually far more efficient than gilmore, some further improvements are worthwhile. In prawitz we prenexed the formula and replaced formerly universally quantified variables with fresh ones at once, then expanded the DNF completely. Instead, we can do all these things incrementally. Suppose we have a set of assumptions to refute. If it contains two complementary literals p and −p, we are already done. Otherwise we pick a non-atomic assumption and deal with it as follows:

  • for p ∧ q, separately assume p and q;
  • for p ∨ q, perform two refutations, one assuming p and one assuming q;
  • for ∀x. P [x], introduce a new variable y and assume P [y], but also keep the original ∀x. P [x] in case multiple instances ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required