%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Encoding for ideal extension
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The program ADM:
%
%% guess set S \subseteq A
% in(X) :- not out(X), arg(X).
% out(X) :- not in(X), arg(X).
%% cf
% :- in(X), in(Y), att(X,Y).
%% argument x is defeated by S
% def(X) :- in(Y), att(Y,X).
%% admissible
% :- in(X), att(Y,X), not def(Y).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% ADM_{in}^bc, where
% d_inIn stands for d_in^in
% d_outIn stands for d_out^in
% d_defeatedIn stands for d_def^in
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c :- not i.
i :- not c.
%% guess
d_inIn(X,Y) :- c, not d_outIn(X,Y), arg(X), arg(Y).
d_outIn(X,Y) :- c, not d_inIn(X,Y), arg(X), arg(Y).
%% cf
:- c, d_inIn(X,Z), d_inIn(Y,Z), att(X,Y).
%% defeated argument x
d_defeatedIn(X,Z) :- c, d_inIn(Y,Z), att(Y,X).
%% adm
:- c, d_inIn(X,Z), att(Y,X), not d_defeatedIn(Y,Z).
%% brave consequence
:~ not d_inIn(X,X), arg(X).
:~ i.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% auxiliary rules for ideal semanitcs
%% in_minus\1 stands for X_F^-
%% in_plus\1 stands for X_F^+
%% q\2 stands for R^*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
in(X) :- d_inIn(X,X).
in_minus(X) :- arg(X), not in(X).
not_in_plus(X) :- in(Y), att(X,Y).
not_in_plus(X) :- in(Y), att(Y,X).
in_plus(X) :- in(X), not not_in_plus(X).
q(X,Y) :- att(X,Y), in_plus(X), in_minus(Y).
q(X,Y) :- att(X,Y), in_minus(X), in_plus(Y).
%% defining an order over in+\1
lt(X,Y) :- in_plus(X),in_plus(Y), X