% file:    truth.pro
% author:  Robert Keller
% purpose: truth checker for first-order predicate logic formulas
%          over a finite interpretation
%
% This is not a general truth checker, as the problem is generally 
% undecidable. It will check truth of a formula over a *specific*
% interpretation with a *finite domain*. The general case would allow
% arbitrary interpretations over any domain, finite or infinite.
%
% The current version does not support function symbols.
% Predicates, constants, and variables are supported.
% 
% Syntax: A Formula is one of the following:
%     forall(Var, Formula)
%     exists(Var, Formula)
%     and(Formula1, Formula2)
%     or(Formula1, Formula2)
%     implies(Formula1, Formula2)
%     iff(Formula1, Formula2)
%     not(Formula)
%     AtomicFormula
%
% An AtomicFormula is one of the following:
%     Predicate(ListOfTerms)
%
% A Predicate is any Prolog symbol.
%
% A ListOfTerms is either: 
%     Term 
%     Term, ListOfTerms
%
% A Term is either:
%     Constant
%     Variable
% (as noted, Terms with function symbols may be added in the future)
%
% A Constant is any Prolog symbol.
% A Variable is any Prolog variable.
%
% Thus Variables must begin with upper-case, and constants must not.
%
% Interpretations: An Interpretation consists of a Domain and a Predicates list.
% A Domain consists of a finite list of Prolog symbols, e.g.
%     [a, b, c]
% Each constant used in a Formula should also be in the Domain.
% The predicate list should be a list of Prolog terms, each indicating
% an AtomicFormula that is true under the interpretation, e.g.
%    [p(a, b), p(a, c), p(b, c)]

% truth(Formula, Domain, Predicates) succeeds when Formula is true
% in the interpretation Domain, Predicates and fails otherwise.
%
% If the formula contains free variables, truth is based on the convention
% that the formula is true iff the equivalent formula with the free variables
% *universally* quanitified is true.

% If Formula contains a free Variable, then to be true, it must be true for each
% substitution of a Domain value for that Variable. 
% Note that this rule will be applied recursively if the formula contains
% more than one free variable.

truth(Formula, Domain, Predicates) :-
    freeVar(Formula, Var),
    !,
    forEachSubstitution(Domain, Var, Formula, Domain, Predicates).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Below, each rule assumes there are NO Free Variables, as 
% such would have been eliminated by the preceding rule.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% If a Formula is of the form forall(Var, Body), then it is true iff
% Body is true for each substitution of a Domain value for Var.

truth(forall(Var, Body), Domain, Predicates) :-
    !,
    forEachSubstitution(Domain, Var, Body, Domain, Predicates).

% If a Formula is of the form exists(Var, Body), then it is true iff
% Body is true for some substitution of a Domain value for Var.

truth(exists(Var, Body), Domain, Predicates) :-
    !,
    forSomeSubstitution(Domain, Var, Body, Domain, Predicates).

% If a Formula is of the form and(F, G), then it is true iff
% both F and G are true. (Recall, no free variables.)

truth(and(F, G), Domain, Predicates) :-
    !,
    truth(F, Domain, Predicates),
    truth(G, Domain, Predicates).

% If a Formula is of the form or(F, G), then it is true iff
% one of F or G is true. (Recall, no free variables.)

truth(or(F, G), Domain, Predicates) :-
    !,
    (
      truth(F, Domain, Predicates)
    ; truth(G, Domain, Predicates)
    ).

% If a Formula is of the form implies(F, G), then it is true iff
% F is not true or G is true. (Recall, no free variables.)

truth(implies(F, G), Domain, Predicates) :-
    !,
    (
    \+truth(F, Domain, Predicates)
    ; truth(G, Domain, Predicates)
    ).

% If a Formula is of the form iff(F, G), then it is true iff
% both F and G are true or neither is. (Recall, no free variables.)

truth(iff(F, G), Domain, Predicates) :-
    !,
    (
      (
      truth(F, Domain, Predicates),
      truth(G, Domain, Predicates)
      )
    ;
      (
      \+truth(F, Domain, Predicates),
      \+truth(G, Domain, Predicates)
      )
     ).

% If a Formula is of the form not(F), then it is true iff
% F is not true. (Recall, no free variables.)

truth(not(F), Domain, Predicates) :-
    !,
    \+truth(F, Domain, Predicates).

% An AtomicFormula is true iff it appears in the Predicates list
% (Recall, no free variables.)

truth(Formula, _Domain, Predicates) :-
    atomicFormula(Formula),
    member(Formula, Predicates).


% Support predicates.

% forEachSubstitution(Values, Var, Formula, Domain, Predicates)
% is true if Formula is true for every substitution of 
% Value in Values.

forEachSubstitution([], _Var, _Formula, _Domain, _Predicates).
    
forEachSubstitution([Value | Values], Var, Formula, Domain, Predicates) :-
    substitute(Value, Var, Formula, Result),
    truth(Result, Domain, Predicates),
    forEachSubstitution(Values, Var, Formula, Domain, Predicates).

% forSomeSubstitution(Values, Var, Formula, Domain, Predicates)
% is true if Formula is true for some substitution of 
% Value in Values.

forSomeSubstitution([], _Var, _Formula, _Domain, _Predicates) :- fail.

forSomeSubstitution([Value | Values], Var, Formula, Domain, Predicates) :-
    substitute(Value, Var, Formula, Result),
    (
      truth(Result, Domain, Predicates)
    ; forSomeSubstitution(Values, Var, Formula, Domain, Predicates)
    ).


% subsitute(Value, Var, Formula, Result) returns as a Result the
% result of substituting Value for Var in Formula.
% Note that care must be taken in the case of Var occurs in Formula,
% which may limit the scope of Var.

% Handle the substitution into a Constant term

substitution(_Value, _Var, Constant, Constant) :-
    atomic(Constant).

% Handle the substitution into a Variable term

substitute(Value, Var, Var2, Result) :-
    var(Var2),
    (
    Var == Var2 ->
      Result = Value
    ; Result = Var2
    ).

% Handle the substitution into a universally-quantified formula

substitute(Value, Var, forall(Var2, Inner), forall(Var2, Inner2)) :-
    Var == Var2 ->
       Inner2 = Inner
    ;  substitute(Value, Var, Inner, Inner2).      
    
% Handle the substitution into a existentially-quantified formula

substitute(Value, Var, exists(Var2, Inner), exists(Var2, Inner2)) :-
    Var == Var2 ->
       Inner2 = Inner
    ;  substitute(Value, Var, Inner, Inner2).      
    
% Handle the substitution into formulas with propositional connectives
% at the top level.

substitute(Value, Var, and(F, G), and(F2, G2)) :-
    substitute(Value, Var, F, F2),
    substitute(Value, Var, G, G2).

substitute(Value, Var, or(F, G), or(F2, G2)) :-
    substitute(Value, Var, F, F2),
    substitute(Value, Var, G, G2).

substitute(Value, Var, implies(F, G), implies(F2, G2)) :-
    substitute(Value, Var, F, F2),
    substitute(Value, Var, G, G2).

substitute(Value, Var, iff(F, G), iff(F2, G2)) :-
    substitute(Value, Var, F, F2),
    substitute(Value, Var, G, G2).

substitute(Value, Var, not(F), not(F2)) :-
    substitute(Value, Var, F, F2).

% Handle substitution into other atomic formulas
% Substitution is done for each argument.

substitute(Value, Var, Formula, Result) :-
    atomicFormula(Formula),
    substituteArgs(Value, Var, Formula, Result).


% Handle substitution into the arguments of an atomic formula.

substituteArgs(Value, Var, Formula, Result) :-
    Formula =.. [Functor | Args],
    substituteEach(Args, Value, Var, NewArgs),
    Result =.. [Functor | NewArgs].


% substitute Value for Var in each of a list of arguments,
% returing a list.

substituteEach([], _, _, []).

substituteEach([Arg | Args], Value, Var, [Result | Results]) :-
    substituteArg(Value, Var, Arg, Result),
    substituteEach(Args, Value, Var, Results).    

substituteArg(Value, Var, Arg, Result) :-
    Var == Arg ->
      Result = Value
    ; Result = Arg.

% Check whether something is an atomic formula by precluding the built-in
% connectives and quantifiers.

atomicFormula(Formula) :-
    builtin(Formula)
    -> fail
    ; true.

builtin(Form) :-
    member(Form, [exists(_, _), forall(_, _), 
                  and(_, _), or(_, _), implies(_, _), iff(_, _), not(_)]).

% Succeed if the formula has at least one free variable.
% Returns that variable if success.

freeVar(exists(Var2, Body), Var) :-
    !,
    freeVar(Body, Var),
    Var \== Var2.

freeVar(forall(Var2, Body), Var) :-
    !,
    freeVar(Body, Var),
    Var \== Var2.

freeVar(and(F, G), Var) :-
    !,
    freeVar(F, Var) ; freeVar(G, Var).

freeVar(or(F, G), Var) :-
    !,
    freeVar(F, Var) ; freeVar(G, Var).

freeVar(implies(F, G), Var) :-
    !,
    freeVar(F, Var) ; freeVar(G, Var).

freeVar(iff(F, G), Var) :-
    !,
    freeVar(F, Var) ; freeVar(G, Var).

freeVar(not(F), Var) :-
    !,
    freeVar(F, Var).

freeVar(Formula, Var) :-
    atomicFormula(Formula),
    Formula =.. [_Functor | Args],
    freeVarArgs(Args, Var).


% Check for free variables in a list of arguments

freeVarArgs([V | _], V) :-
    var(V).

freeVarArgs([_ | More], V) :-
    freeVarArgs(More, V).

test(Expectation, Formula, Domain, Predicates) :-
    nl,
    write('Formula:    '), write(Formula), nl,
    write('Domain:     '), write(Domain), nl,
    write('Predicates: '), write(Predicates), nl,
    write('Result:     '),
    (
    truth(Formula, Domain, Predicates) ->
        write('true'),
        (Expectation -> write(', as expected'), nl
         ; write(', not as expected. TEST FAILURE'), nl
        )
       ; write('false'),
        (Expectation -> write(', not as expected. TEST FAILURE'), nl
         ; write(', as expected'), nl
        )
    ).
      
% Test cases
test1t :-
    test(true, p(a, b), [a, b, c], 
         [p(a, a), p(b, a), p(a, b)]).

test1f :-
    test(false, p(a, b), [a, b, c], 
         [p(a, a), p(b, a), p(b, b)]).

test2t :-
    test(true,
          forall(X, p(a, X)), [a, b, c], 
          [p(a, a), p(a, b), p(b, b), p(b, c), p(a, c)]).

test2f :-
    test(false,
          forall(X, p(a, X)), [a, b, c], 
          [p(a, a), p(a, b), p(b, b), p(b, c), p(c, c)]).

test3t :-
    test(true,
          exists(X, p(a, X)), [a, b, c], 
          [p(b, a), p(a, b), p(b, b), p(b, c)]).

test3f :-
    test(false,
          exists(X, p(a, X)), [a, b, c], 
          [p(b, a), p(b, b), p(b, c)]).

test4t :-
    test(true,
          exists(X, forall(Y, p(X, Y))), [a, b, c], 
          [p(a, a), p(a, b), p(a, c)]).

test4f :-
    test(false,
          forall(X, exists(Y, p(X, Y))), [a, b, c], 
          [p(a, a), p(a, b), p(a, c)]).

test5t :-
    test(true,
          and(p(a, b), p(a, c)), [a, b, c], 
         [p(a, a), p(a, b), p(a, c)]).

test5f :-
    test(false,
          and(p(a, b), p(b, c)), [a, b, c], 
          [p(a, a), p(a, b), p(a, c)]).

test6t :-
    test(true,
          or(p(b, b), p(a, c)), [a, b, c], 
          [p(a, a), p(a, b), p(a, c)]).

test6f :-
    test(false,
          or(p(b, b), p(c, c)), [a, b, c], 
          [p(a, a), p(a, b), p(a, c)]).

test7t :-
    test(true,
          not(p(b, b)), [a, b, c], 
          [p(a, a), p(a, b), p(a, c)]).

test7f :-
    test(false,
          not(p(a, c)), [a, b, c], 
          [p(a, a), p(a, b), p(a, c)]).

test8t :-
    test(true,
          implies(p(b, b), p(c, c)), [a, b, c], 
          [p(a, a), p(a, b), p(a, c)]).

test8f :-
    test(false,
          implies(p(a, b), p(c, c)), [a, b, c], 
          [p(a, a), p(a, b), p(a, c)]).

test9t :-
    test(true,
          forall(X, or(p(X, a), p(a, X))), [a, b, c], 
          [p(a, a), p(a, b), p(a, c)]).

test9f :-
    test(false,
          forall(X, or(p(X, a), p(a, X))), [a, b, c], 
          [p(b, b), p(b, c), p(c, c)]).

test10t :-
    test(true,
          forall(X, p(X, X)), [a, b, c], 
          [p(a, a), p(b, b), p(c, c)]).

test10f :-
    test(false,
          forall(X, p(X, X)), [a, b, c], 
          [p(a, a), p(b, b)]).

test11t :-
    test(true,
          forall(X, and(p(X, a), p(a, X))), [a, b, c], 
          [p(a, a), p(a, b), p(b, a), p(a, c), p(c, a)]).

test11f :-
    test(false,
          orsome(x, and(p(X, a), p(a, X))), [a, b, c], 
          [p(b, a), p(a, c), p(c, b)]).

test12t :-
    test(true,
          forall(X, implies(p(X, a), p(a, X))), [a, b, c], 
          [p(a, a), p(b, a), p(a, b), p(c, a), p(a, c)]).

test12f :-
    test(false,
          forall(X, implies(p(X, a), p(a, X))), [a, b, c], 
          [p(b, a), p(c, b), p(b, c)]).

test13t :-
    test(true,
          forall(X, implies(p(X, a), p(a, X))), [a, b, c], 
          [p(a, b), p(b, b), p(b, c)]).

test13f :-
    test(false,
          forall(X, implies(p(X, a), p(X, X))), [a, b, c], 
          [p(b, a), p(b, c)]).

test14t :-
    test(true,
          forall(X, iff(p(X, a), p(X, b))), [a, b, c], 
          [p(a, a), p(a, b), p(b, b), p(b, a)]).

test14f :-
    test(false,
          forall(X, iff(p(a, X), p(b, X))), [a, b, c], 
          [p(a, b), p(b, c)]).

test :-
    test1t,
    test1f,
    test2t,
    test2f,
    test3t,
    test3f,
    test4t,
    test4f,
    test5t,
    test5f,
    test6t,
    test6f,
    test7t,
    test7f,
    test8t,
    test8f,
    test9t,
    test9f,
    test10t,
    test10f,
    test11t,
    test11f,
    test12t,
    test12f,
    test13t,
    test13f,
    test14t,
    test14f,
    true.