2.1.7 Evaluating Complex Formulae

Designing the first version of actual model checker program, which evaluates (representations of) formulae in (representations of) models: Evaluating complex formulas.

Now let's have a look at the clauses for Boolean combinations of formulae. First for the binary connectives:

eval(Formula1 & Formula2,Model):-
   eval(Formula1,Model),
   eval(Formula2,Model).

eval(Formula1 v Formula2,Model):-
   eval(Formula1,Model);
   eval(Formula2,Model).

eval(Formula1 > Formula2,Model):-
   eval(Formula2,Model);
   \+ eval(Formula1,Model).

Truth Conditions in Prolog.

These clauses mirror the first-order satisfaction definition (on which the definition of truth in a model is based) in an obvious way, using the Prolog versions of conjunction, disjunction and negation. For example, the clause for > translates to Prolog that an implication is true iff:

• the consequent is true, or

• the antecedent is false.

Negation and Prolog Negation.

We make use of Prolog negation (that is, negation as failure) when we want to evaluate negated formulae. This is a simple and natural thing to do. However we shall see soon that it can have unexpected - and unintended - effects. Here's the code:

eval(~Formula,Model):-
   \+ eval(Formula,Model).