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

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.

No credit card required