2.2.1 Problem One: Unknown Vocabulary

Problems when verifying formulae that use completely new non-logical vocabulary.

What happens if our input uses symbols that are not in our vocabulary? We run into problems if we ask our model checker to verify formulae that use completely new non-logical vocabulary.

For example, there's no constant symbol cinderella in our vocabulary. Let's try to evaluate the formula , say in model 5. The formula states that ``Everyone is a therapist, but Cinderella isn't.'' Clearly, this is contradictory. So whenever well-formed, this formula is unsatisfiable. It should thus never come out as true, no matter in which model we choose to evaluate it. So let's query evaluate(forall(x,therapist(x)) & ~therapist(cinderella), 5). Surprisingly the answer is yes. How could this happen?

Let us have a short look at a simpler example. Let's call evaluate(therapist(cinderella),5). Our model checker says no. This response, too, is not strictly speaking correct. Formally the satisfaction relation (and thus truth) is not defined for formulae and models of different vocabularies. The correct response of our model checker would be to reject this formula and say something like ``Hey, I don't know anything about the symbol cinderella!''.

This little flaw may seem harmless at first glance, but the same problem leads to the false positive we've seen above. Think about what our model checker does when it evaluates forall(x,therapist(x)) & ~therapist(cinderella) in a given model: First it checks if forall(x,therapist(x)) is true in our model. (Remember the Prolog clause for universal quantification: The model checker will check that ~exists(x, ~therapist(x)) is true, by making sure that therapist(c) isn't false for any of the const(c) in the database). In model 5, this is the case. Then, our program proceeds to the second conjunct. There it finds the negation ~therapist(cinderella), which it evaluates using Prolog's \+: ~therapist(cinderella) will become true if evaluating therapist(cinderella) fails. And in fact evaluating therapist(cinderella) does fail. Yet this not due to the situation in our model, but simply because cinderella is not in the vocabulary: therapist(cinderella) is not one of the facts that don't occur on our list because they are false. Rather, it does not come into consideration as a positive or as a negative fact at all, because it is not well-formed.

The moral is that the use of negation as failure may turn a somewhat sloppy no (like the answer of our model checker to unknown vocabulary) into a dangerously clear yes. So we really should take care that no really only means ``not true''.

Luckily the problem is not particularly deep; the solution is simply to be explicit about what a well formed formula over a given vocabulary is. That is, we should make use of the information in the vocabulary about which predicate symbols we are working with (and, of course, what their arities are), which constants we have, and explicitly state which combinations of these symbols are well formed. Our driver should check that any sequence of symbols it has to evaluate really is a well formed combination of the chosen predicate and constant symbols - and it should refuse to evaluate anything that isn't.