10.4.1 A New Problem

A problem with known individuals and witnesses.

How do our rules fare if we want to generate models with our tableaux calculus? There's no problem with the -rule. Obviously, a model for a universal quantification may - in fact even has to - contain all the literals that come from any instance of the scope. And our rule allows to derive all of them (one after another). Let us look at a tableaux for ``Mutz is a siamese cat and Tiger is a siamese cat'', where we know that ``Every siamese cat purrs'' (to get a smaller tableaux, we use the derived inference rule for implication from Section 7.2.8):

A model that we like

The only branch that finally remains open on this tableaux contains a model where our world knowledge about purring siamese cats has been applied to Mutz as well as to Tiger: Both purr.

But now let's turn to the -rule. Let's look at a tableaux for the discourse ``Mutz is asleep. Tiger isn't purring. There is a siamese cat that's purring.'' We get the following tableaux:

A model that we don't like

This is a little disappointing. Of course we have generated a model for our input formula, but we have learned nothing new about Mutz or Tiger. Instead our calculus has invented a brand new siamese cat, and tells us that this cat purrs.

The problem

The core problem is that our -rule is designed to introduce a new constant every time it is applied. In effect it only generates models that have a new individual for each existential quantification. Such models are often strongly non-minimal. Non-minimality doesn't matter for theorem proving. But in model generation, we also want to get smaller models where existential quantifications are instantiated with individuals that are already there in the model. As we've convinced ourselves, we cannot achieve this by simply instantiating with one of the individuals that are already on the tableau. Otherwise we could incidentally say something wrong about that individual, introducing an unwarrranted contradiction (e.g. notice that if we had instantiated with on the above tableaux, we would have closed it without any good reason).


Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos
Version 1.2.5 (20030212)