ground.dl

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Encoding for grounded extensions
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% an argument x defeats an argument y if x attacks y
defeat(X,Y) :- att(X,Y).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% For the remaining part we need to put an order on the domain.
% Therefore, we define a successor-relation with infinum and supremum 
% as follows 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

lt(X,Y) :- arg(X),arg(Y), X<Y, not input_error.
nsucc(X,Z) :- lt(X,Y), lt(Y,Z).
succ(X,Y) :- lt(X,Y), not nsucc(X,Y).
ninf(X) :- lt(Y,X).
nsup(X) :- lt(X,Y).
inf(X) :- not ninf(X), arg(X).
sup(X) :- not nsup(X), arg(X).

%% we now fill up the predicate in(.) with arguments which are defended

defended_upto(X,Y) :- inf(Y), arg(X), not defeat(Y,X).
defended_upto(X,Y) :- inf(Y), in(Z), defeat(Z,Y), defeat(Y,X).
defended_upto(X,Y) :- succ(Z,Y), defended_upto(X,Z), not defeat(Y,X).
defended_upto(X,Y) :- succ(Z,Y), defended_upto(X,Z), in(V), defeat(V,Y), defeat(Y,X).

defended(X) :- sup(Y), defended_upto(X,Y).
in(X) :- defended(X).