%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% main.lp
%%
%% (C) Thomas Linsbichler, Jörg Pührer, Hannes Strass, 2015
%%
%% Deciding realisability of sets of three-valued interpretations
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% main encoding
% s/1 declares statements
% in/1 declares (user-given) whether interpretations are desired
% the respective semantics encodings declare an internal predicate inV/1
syntax_error(I) :- in(I), not int(I).
%#show syntax_error/1.
% a cterm is an assignment of a truth value to a statement
cterm(S, t(S)) :- s(S).
cterm(S, f(S)) :- s(S).
% int/1 declares interpretations
% an interpretation is an ordered list of assignments of statements to one of two truth values
% if a statement is not assigned a truth value, it is assumed it gets u
int(nil).
int((ST, I)) :-
s(S),
cterm(S, ST),
int(I),
smaller(S, I).
% assigning a statement a truth value can only be done at the beginning of a list if the assigned statement is smaller than the smallest already assigned statement
smaller(S, nil) :- s(S).
smaller(S, (H, I)) :-
s(S),
cterm(T, H),
S < T,
int(I).
% check whether an assignment is contained in an interpretation
member(T, (T, I)) :- int((T, I)).
member(T, (X, I)) :- int((X, I)), member(T, I).
% an interpretation is two-valued
int2(I) :- int(I), not hasU(I).
hasU(I) :- hasU(I, S).
hasU(I, S) :- int(I), s(S), not member(t(S), I), not member(f(S), I).
% the information ordering on interpretations
ileq(I, J) :- int(I), int(J), not nileq(I, J).
nileq(I, J) :- int(I), int(J), member(T, I), not member(T, J).
% the two classical truth values
tv(t).
tv(f).
% now guess acceptance conditions
1 { ac(S, I, V) : tv(V) } 1 :- s(S), int2(I).
% show: the output predicate for realisability is the one defining the acceptance functions
% #show ac/3.