*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 ...

Start Free Trial

No credit card required