/* DIVIDE.

Test example for SEMANT and MODEL
Clauses and Model for not divides example (see notes p124)

Alan Bundy  22.6.81 */

/* Clauses */

clause(right, [not_div(X*Z,Y)], [not_div(X,Y)], input). % Input clauses

clause(left, [not_div(Z*X,Y)], [not_div(X,Y)], input).

clause(thirty, [equal(30,2*3*5)], [], input).

clause(hypothesis, [not_div(5,a)], [], input).


clause(conclusion, [], [not_div(30,a)], topclause).     % Top clause




/* Models */

/* arith2 */

interpretation(arith2).         % arith2 is an interpretation

interpret(arith2, a, 2).                        % meaning of a

interpret(arith2, not_div(X,Y), false) :-       % meaning of not_div
        0 is Y mod X, !.
interpret(arith2, not_div(X,Y), true).

interpret(arith2, equal(X,Y), true) :-          % meaning of equal
        X =:= Y, !.
interpret(arith2, equal(X,Y), false).

interpret(arith2, X*Y, Z) :- Z is X*Y.          % meaning of *



/* arith3 */

interpretation(arith3).         % arith3 is an interpretation

interpret(arith3, a, 3).                        % meaning of a

interpret(arith3, not_div(X,Y), false) :-       % meaning of not_div
        0 is Y mod X, !.
interpret(arith3, not_div(X,Y), true).

interpret(arith3, equal(X,Y), true) :-          % meaning of equal
        X =:= Y, !.
interpret(arith3, equal(X,Y), false).

interpret(arith3, X*Y, Z) :- Z is X*Y.          % meaning of *