/*************************************************************************
%% Based on:
         name: modelChecker.pl
  description: A model checker for first-order logic.
      authors: Patrick Blackburn & Johan Bos

%% Modified and adapted by stwa July, 2002
 
*************************************************************************/

:- module(modelChecker,[evaluate/2]).

:- user:[comsemOperators].

:- use_module(exampleModels,[example/2]).

:- use_module(signature,[const/1]).

:- use_module(substitute,[subst/3]).

/*========================================================================
   Evaluate a formula in a model
========================================================================*/

evaluate(Formula,ExampleNumber):-
   example(ExampleNumber,Model),
   eval(Formula,Model).

/*========================================================================
   Semantic Evaluation
========================================================================*/

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

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).

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

eval(exists(X,Formula),Model):-
   const(C),
   subst([X:C],Formula,Instantiated),
   eval(Instantiated,Model).

eval(forall(X,Formula),Model):-
   eval(~ exists(X,~ Formula),Model).