%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% af.lp
%%
%% (C) Thomas Linsbichler, Jörg Pührer, Hannes Strass, 2015
%%
%% Deciding realisability of sets of three-valued interpretations
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% AF realisability
% the truth ordering on three-valued interpretations
% a/ka the subset ordering on two-valued interpretations
tleq(I, J) :- int2(I), int2(J), not ntleq(I, J).
ntleq(I, J) :- int2(I), int2(J), s(S), member(t(S), I), not member(t(S), J).
% in an AF realisation, the acceptance condition of each statement S must be such that:
% the set of disjuncts is upward-closed with respect to the least upper bound of the truth ordering
tcup(I, J, K) :- uppertbound(I, J, K), not smalleruppertbound(I, J, K).
uppertbound(I, J, K) :- tleq(I, K), tleq(J, K).
smalleruppertbound(I, J, K) :- uppertbound(I, J, K), int2(L), uppertbound(I, J, L), tleq(L, K), not tleq(K, L).
ac(S, K, t) :- ac(S, I, t), ac(S, J, t), tcup(I, J, K).
% the set of true disjuncts is downward-closed with respect to the truth ordering
ac(S, J, t) :- ac(S, I, t), tleq(J, I).
% in particular, the least element of the truth ordering is contained in every disjunct
tleast(I) :- int2(I), not tsmaller(I).
tsmaller(I) :- int2(I), int2(J), tleq(J, I), not tleq(I, J).
ac(S, I, t) :- s(S), tleast(I).
% the set of false disjuncts is upward-closed with respect to the truth ordering
ac(S, J, f) :- ac(S, I, f), tleq(I, J).
%#show tleq/2.