%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% prf.lp
%%
%% (C) Thomas Linsbichler, Jörg Pührer, Hannes Strass, 2015
%%
%% Deciding realisability of sets of three-valued interpretations
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% preferred semantics
% only ileq-antichains (w.r.t. the original interpretations) are realisable in principle
:- in(I), in(J), ileq(I, J), nileq(J, I).
inV(I) :- in(I).
% the constraints below are as for admissible, but we can simply guess additional, adm-induced desired interpretations
{ inV(J) } :- in(I), ileq(J, I), nileq(I, J).
% members
:- int(I), inV(I), s(S), member(t(S), I), int2(J), ileq(I, J), ac(S, J, f).
:- int(I), inV(I), s(S), member(f(S), I), int2(J), ileq(I, J), ac(S, J, t).
alwaysFalse2(I, S) :-
int(I),
s(S),
not onceTrue2(I, S).
onceTrue2(I, S) :-
ileq(I, J),
int2(J),
ac(S, J, t).
alwaysTrue2(I, S) :-
int(I),
s(S),
not onceFalse2(I, S).
onceFalse2(I, S) :-
ileq(I, J),
int2(J),
ac(S, J, f).
% non-members
:- int(I), not inV(I), not existsCounterExample(I).
existsCounterExample(I) :- existsCounterExample(I, S, J).
existsCounterExample(I, S, J) :-
s(S),
member(t(S), I),
int2(J),
ileq(I, J),
ac(S, J, f).
existsCounterExample(I, S, J) :-
s(S),
member(f(S), I),
int2(J),
ileq(I, J),
ac(S, J, t).