2.2.3 Refining the Implementation

Solving the problems of our first implementation of the modelchecker.

revisedModelChecker.pl: View Download

So let's re-visit our implementation and modify it according to our new insights. The simplest we can do is to modify our driver predicate as follows:

evaluate(Formula,ExampleNumber):-
   example(ExampleNumber,Model),
   wff(Formula),           % Implement as an exercise
   free(Formula,[]),       % Imported from module substitute
   eval(Formula,Model).

eval(Formula,Model):-
   member(Formula,Model).

In this piece of code wff/1 is a predicate that checks whether a given formula is well-formed over the vocabulary in the database. You should implement this predicate as an exercise.

substitute.pl: View Download

The call free(Formula,[]) solves our second problem: It enforces that the input Formula contains no free variables, hence that it really is a sentence. The predicate free/2 (coming from substitute.pl) produces the list of unbound variables in the formula given as first argument. Hence calling it with an empty list as second argument makes sure that there are no free variables in the formula given as first argument.

We said before that we have to make sure that no really only means ``not true''. But up to now, we have not done so. We have only moved the no meaning ``unexpected input'' to the beginning of our predicate, where it cannot interfere with the no meaning ``not true''. However it is now a simple task to exit with a message on unexpected input before the actual model checking is started. Exercise 2.9 asks you to implement this little error-handling capability.

In revisedModelChecker.pl you find an incomplete implementation of the revised model checker: The (unchanged) clauses of eval/2, rev_evaluate/2 as discussed above, and a dummy predicate wff/1 that you can replace by your implementation from Exercise 2.2.


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