%Andreas van Cranenburgh, 0440949
%Test a Discourse Representation Structure (DRS) on a model.
% A DRS consists of a list of variables and a list of conditions (predicates or
%DRSes). Eg. drs([X], [duck(X)]).
%A model consists of a list of constants (atoms) and a list of
%predicates applied on those constants. Eg. model([a], [duck(a)]).

%remove double negation
true(not(not(DRS)), Model) :-
	true(DRS, Model).

%Negation
true(not(drs(Ref, Cond)), model(Obj, Formulas)) :-
	\+ true(drs(Ref, Cond), model(Obj, Formulas)).

/*
true(not(drs(Ref, Cond)), model(Obj, Formulas)) :-
	subset1(Ref, Obj),
	forall(member(X, Cond),
		(\+ (member(X, Formulas)
		; true(X, model(Obj, Formulas))))).
*/

%Implication ( A => B equals ~(A ^ ~B))
true(imp(drs(Ref1, Cond1), drs(Ref2, Cond2)), Model) :-
	true(not(drs([], [drs(Ref1, Cond1), not(drs(Ref2, Cond2))])), Model).

%true(imp(DRS1, DRS2), Model) :-
%	(true(DRS1, Model) ->
%		true(DRS2, Model)
%		; true(not(DRS1), Model)).

%Condition is part of model, or is a DRS valid on model.
true(drs(Ref, Cond), model(Obj, Formulas)) :-
	subset1(Ref, Obj),
	forall(member(X, Cond),
		member(X, Formulas)
		;
		true(X, model(Obj, Formulas))).

%Modified subset predicate which creates bindings of variables,
%and allows backtracking.
subset1([], _).
subset1([A|C], B) :-
	member(A, B),
	subset1(C, B).

%Example queries
go1 :-
	true(
		drs([X, Y], [jan(X), ezel(Y), heb(X, Y), sla(X, Y)]),
		model([a,b,c,d], [ezel(b), ezel(c), jan(a), heb(a,c), heb(d,b), sla(a,c), sla(d,b)])
	),
	writef('X = %w,\nY = %w.', [X, Y]).

go2 :-
	true(
		drs([X,Y], [imp(
			drs([], [boer(X), ezel(Y), heb(X, Y)]),
			drs([], [sla(X, Y)]))]),
		model([a,b,c,d], [ezel(b), ezel(c), boer(a), heb(a,c), heb(d,b), sla(a,c), sla(d,b)])
	),
	writef('X = %w,\nY = %w.', [X, Y]).

go3 :-
	true(
		drs([X], [jongen(X), not(drs([], [slaap(X)]))]),
		model([a,b], [jongen(a), jongen(b), slaap(a)])
	),
	writef('X = %w', [X]).

go4 :-
	true(
		drs([X], [not(drs([], [jongen(X), slaap(X)]))]),
		model([a,b], [jongen(a), jongen(b), slaap(a)])
	),
	writef('X = %w', [X]).