/* MODEL. How to evaluate a clause in an interpretation (provided it is variable free!!) use with SEMANT DIVIDE contains test examples Alan Bundy 22.6.81 */ /* Vet the clause in any interpretations */ vet(Clause) :- not satisfiable(Clause). % Clause has no model /* Clause is satisfiable in some Interpretation */ satisfiable(Clause) :- interpretation(Interp), % If there is an interpretation model(Interp,Clause), % in which Clause is true writef('%t rejected by %t\n\n',[Clause,Interp]). % tell user /* Interpretation is a model of a Clause */ model(Interp, Clause) :- clause(Clause,Consequent,Antecedent,_), % Get Clause definition checklist(is_true(Interp), Consequent), % Check all lhs literals are true checklist(is_false(Interp), Antecedent). % and all rhs ones are false /* Evaluate expression in Interpretation */ evaluate( Interp, Integer, Integer ) :- integer(Integer), !. % integers represent themselves evaluate( Interp, Constant, Value ) :- % other constants have values assigned atom(Constant), !, interpret(Interp, Constant, Value). evaluate( Interp, Complex, Value ) :- Complex =.. [Sym | Args], !, % recurse on arguments of maplist(evaluate(Interp), Args, Vals), % complex terms Complex1 =.. [Sym | Vals], % then interpret topmost interpret(Interp, Complex1, Value). % symbol /* Evaluation of clause (hacks for checklist) */ is_true(Interp, Literal) :- evaluate(Interp, Literal, true). is_false(Interp, Literal) :- evaluate(Interp, Literal, false).