| << Prev | - Up - | Next >> |
Designing the first version of actual model checker program, which evaluates (representations of) formulae in (representations of) models: Evaluating simple formulas.
We now turn to the fourth and final task: Designing the actual model checker program, which evaluates (representations of) formulae in (representations of) models. That is, our program should say yes if the input formula is true in the given model and no if it isn't. E.g. given our first example model and the formula therapist(john) & moron(peter), the program should answer yes. In contrast, evaluating therapist(john) & therapist(peter) over the same model should lead to the answer no.
We now write a predicate called eval/2 to carry out this task. It consists of seven clauses and takes two arguments: First the formula to be tested, and second the model in our list representation. As discussed above we assume that the vocabulary can be found in the database.
modelChecker.pl: View Download
The clauses of eval/2 and (a driver predicate evaluate/2, see Section 2.1.9) can be found in modelChecker.pl.
Evaluating Atomic Formulas
First for the core of our little model checker. The clause that evaluates atomic formulae. It couldn't be much simpler. We have decided to represent an exact model by recording all the facts (in the form of atomic formulae) that are true in it. Hence an atomic formula is true if and only if it is one of the facts recorded in the list Model. So all we need to do is search through our list:
eval(Formula,Model):-
member(Formula,Model).
| << Prev | - Up - | Next >> |