/*************************************************************************
         name: revisedModelChecker.pl
  description: Revised version of model checker for first-order logic.
      authors: Stephan Walter, Patrick Blackburn & Johan Bos
      version: July, 2002    
 
*************************************************************************/

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

:- ensure_loaded(comsemOperators).

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

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

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

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

evaluate(Formula,ExampleNumber):-
   example(ExampleNumber,Model),
   wff(Formula),           % Implement as an exercise
   free(Formula,[]),       % Imported from module substitute
   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).


/*========================================================================
   Replace by your own implementation
========================================================================*/

%wff(Formula) :-
%	write('Not yet implemented'),
%	nl.