2.1.8 Quantifiers
Designing the first version of actual model checker program, which evaluates (representations of) formulae in (representations of) models: Quantifiers.
The clause for the existential quantifier also quite directly implements the respective part of the satisfaction definition. Our program picks one entity from the model and instantiates the quantified variable X to it.:
eval(exists(X,Formula),Model):-
const(C),
subst([X:C],Formula,Instantiated),
eval(Instantiated,Model).
Instantiating the Quantified Variable.
Now because we work with exact models and assume our universe to consist of constants, to pick one entity simply means to access the vocabulary and choose a constant.
For this task we use the predicate subst/3 from substitute.pl. It takes a substitution (of the form [Substitute1:By1,Substitute2:By2...]) and applies it to the Formula given as second argument. The third arguments contains the result. The code for subst/3 is a bit more involved than you might expect, because it implements full first-order substitution . For the case at hand, though, it simply recurses down to literals, splits them and finally replaces the arguments according to the given substitution.
Backtracking on Instantiations.
Then, our program tests if the now instantiated Formula is true in the given model. If this is not the case, the program backtracks and tries another constant. Either it eventually succeeds. This means that our existential quantification is true because there exists an entity that supports the scope (after all our program has found one such entity). Or it doesn't succeed, which means that the existential quantification is false.
The clause for the universal quantifier takes advantage of a logical equivalence: 
is equivalent to 
. So instead of forall(X, Formula) we can equivalently consider ~exists(X, ~Formula). This is what happens in the following clause.
eval(forall(X,Formula),Model):-
eval(~ exists(X,~ Formula),Model).
If you like to, you can prove the equivalence used by this clause as Exercise 2.7