10.2.3 Restricting the Application of the Universal Rule

Restricting the Application of the Universal Rule.

There may be infinitely many individuals.

But we immediately run into the next trouble. The interplay between - and -quantifiers may introduce infinitely many new individuals to a tableaux. Consequently the two input formulae and would be enough to let our program (in its present form) go off forever generating fathers . We have to control when and how often is (re-)applied .

Limiting instantiations

The solution to this is simple: We allow each quantifier only a limited number of instantiations. This is what the third new argument of tabl/6 (Qdepth) is for: It formulates the upper bound on the number of instantiations.

Completeness lost

It is important to understand that this solution makes our algorithm incomplete: It may always happen that we only allow for n instantiations, where the (n+1)th instantiation would have closed our tableaux. So, we might fail to find out that some formula is a theorem only because we have stopped our tableau construction process too early. Still there is one thing we can do: We can use iterative-deepening . That means we can increase our Qdepth and re-run the tableaux construction (e.g. during lunchtime) to get a more exhaustive result. Iterating this process, we can approximate completeness, and this is all we can hope for. As we've discussed, there's a price we have to pay for the expressivity of first order logic: Satisfiability (and validity) is no longer decidable. Therefore no terminating implementation of a first-order calculus can ever be complete.

New instantiations

It is clever to make sure that a new instantiation is generated each time we expand a universal quantifier. One does not want to waste Qdepth on generating the same instantiations twice or more. We ensure this by attaching a list to each quantifier on our quants-list that records which individuals have already been used with some particular quantifier. So, each quantifier is put on the quants-list in a tuple of the form:

(forall(X,Scope),Inds)

The list Inds tells us to which individuals have already been used with the quantifier. At the same time we can read off the list how often it has been instantiated in total.