%%% version 1.0-2

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%                 {log} library predicates
%       for dealing with problems from the TPTP library
%
%                           Version 1.0
%
%           by Maximiliano Cristia' and  Gianfranco Rossi
%                           October 2018
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- add_lib('setloglibpf.slog').

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% all bibligraphic references given in the comments can be 
% found at 
% http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Documents&File=Bibliography.bib
%
% tba, pixley, pixleyd and nand are Boolean algebra operators
% defined over variables whose values are finite sets
% instead of Booleans
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Ternary Boolean Algebra
% tba(X,Y,Z,T) <=> multiply(X,Y,Z) = T
%
tba(X,Y,Z,T) :-
  inters(X,Y,M1)
  & inters(Y,Z,M2)
  & inters(Z,X,M3)
  & un(M2,M3,M4)
  & un(M1,M4,T).

% pixley(X,Y,Z) is a Pixley polynomial
% pixley(X,Y,Z) = 
%   add(multiply(X,inverse(Y)),add(multiply(X,Z),multiply(inverse(Y),Z)))
% pixley(X,Y,Z,U,T) <=> pixley(X,Y,Z) = T where X, Y and Z
%   are subsets of U
%
pixley(X,Y,Z,U,T) :-
  un(Y,M1,U)
  & disj(Y,M1)
  & subset(X,U)
  & subset(Z,U)
  & inters(X,M1,M2)
  & inters(X,Z,M3)
  & inters(M1,Z,M4)
  & un(M3,M4,M5)
  & un(M2,M5,T).

% Dual of Pixley
%
pixleyd(X,Y,Z,U,T) :-
  un(Y,M1,U)
  & disj(Y,M1)
  & subset(X,U)
  & subset(Z,U)
  & un(X,M1,M2)
  & un(X,Z,M3)
  & un(M1,Z,M4)
  & inters(M3,M4,M5)
  & inters(M2,M5,T).

% nand --> the "not and" operator of Boolean algebra
% nand(X,Y,U,Z) <=> nand(X,Y) = Z where X, Y and Z are subsets of U
%
nand(X,Y,U,Z) :-
   subset(X,U)
   & subset(Y,U)
   & inters(X,Y,M1)
   & diff(U,M1,Z).

% equal to nand but it operates over 'Boolean sets'
% a Boolean sets can be either {} or {{}}
% where {} represents false and {{}} represents true
%
nandb(X,Y,Z) :-
  inters(X,Y,M1)
  & un(M1,Z,{{}})
  & disj(M1,Z).

% X is a 'Boolean set'
%
bool(X) :-
  X = {} or X = {{}}.

% binary relation R is a vector (as defined in Relation Algebra)
%
vec(R,B) :-
  R = cp(M1,B).

% the negation of vec
%
nvec(R,B) :-
  rel(R)
  & set(B)
  & [M1,_] in R
  & M2 in B
  & [M1,M2] nin R.

% unifies the ordered pair [X,Y] with the standard set
% representation of ordered pairs
%
sop([X,Y],{{X},{X,{Y}}}) :-
  nset(X) & nset(Y).

% restricts R to the set of its ordered pairs
% X and Y are assumed to be the sorts for the domain
% and range of R
% restrict is defined in the axiomatization of set 
% theory given in [Qua92]
% in {log} is not really necessary because
% binary relations contain just ordered pairs
%
restrict(R,X,Y,RR) :- 
  inters(R,cp(X,Y),RR).

% the negation of restrict
%
nrestrict(R,X,Y,RR) :- 
  ninters(R,cp(X,Y),RR).

% range is defined in the axiomatization of set 
% theory given in [Qua92]
% Y is an element in the relational image of {X} through R
% U2 is used to give the universal range of R
%
range(R,X,U2,Y) :-
  restrict(R,{X},U2,M1)
  & [M2,Y] in M1.

% domain is defined in the axiomatization of set 
% theory given in [Qua92]
% X is an element such that one of its images through R
% is Y
% U1 is used to give the universal domain of R
%
domain(R,U1,Y,X) :-
  restrict(R,U1,{Y},M1)
  & [X,M2] in M1.

% diagonalise is defined in the axiomatization of set 
% theory given in [Qua92]
% diagonalise(Xr) =
%   complement(domain_of(intersection(Xr,identity_relation)))
% intersec Xr with the identity relation, get the domain of the
% resulting relation and finally get the complement of that set
% S is the diagonal of R
% U is used as the universe for the identity relation 
%
diagonalise(R,U,S) :-
  id(U,M1)
  & dom(M2,M3)
  & un(M3,S,U)
  & disj(M3,S)
  & inters(R,M1,M2).

% first is defined in the axiomatization of set 
% theory given in [Qua92]
% X is the first component of the ordered pair S
% given as a set
%
first(S,X) :-
      S = {{M1},{M1,{M2}}} &
      X = {M1}.
first(S,X) :-
     nonvar(S) &
     naf S = {{M1},{M1,{M2}}} &
     X = S.

% second is defined in the axiomatization of set 
% theory given in [Qua92]
% X is the second component of the ordered pair S
% given as a set
%
second(S,X) :-
      S = {{M1},{M1,{M2}}} &
      X = {M2}.
second(S,X) :-
     nonvar(S) &
     naf S = {{M1},{M1,{M2}}} &
     X = S.

% first1 is defined in the axiomatization of set 
% theory given in [BL+86]
% X is the first component of the ordered pair S
% given as a set
%
first1(S,X) :-
  S = {{M1},{M1,{M2}}}
  & nset(M1)
  & nset(M2)
  & X = {M1}.

% second1 is defined in the axiomatization of set 
% theory given in [BL+86]
% X is the second component of the ordered pair S
% given as a set
%
second1(S,X) :-
  S = {{M1},{M1,{M2}}}
  & nset(M1)
  & nset(M2)
  & X = {M1,{M2}}.

% compatible is defined in the axiomatization of set 
% theory given in [Qua92]
% compatible(xh,xf1,xf2) <=> 
%   function(xh)
%   & domain_of(domain_of(xf1)) = domain_of(xh)
%   & range_of(xh) < domain_of(domain_of(xf2))
%
compatible(F,G,H) :-
  pfun(F)
  & dom(G,M1)
  & dom(M1,M2)
  & dom(F,M2)
  & ran(F,M3)
  & dom(H,M4)
  & dom(M4,M5)
  & subset(M3,M5).

% operation is defined in the axiomatization of set 
% theory given in [Qua92]
% operation(xf) <=> 
%   function(xf) 
%   & cross_product(domain_of(domain_of(xf)),
%                   domain_of(domain_of(xf))) = domain_of(xf)
%   & range_of(xf) < domain_of(domain_of(xf))
%
operation(F) :-
  pfun(F)
  & dom(F,cp(M1,M1))
  & ran(F,M2)
  & subset(M2,M1).

% invimg is defined in the axiomatization of set 
% theory given in [Pas99]
%
% X in inverse_image2(F,B)) <=> 
%   Y in B & apply(F,X,Y)
% invimg(F,B,A) <=> A is the set of elements whose images
%                   through F is B
invimg(F,B,A) :-
  rres(F,B,M1)
  & dom(M1,A).

% C is the set of element related to A through R
%
eclass(R,E,A,C) :-
  inters(R,cp({A},E),M1)
  & ran(M1,C).

% zero is defined in the axiomatization of relation 
% algebra given in [Hoe08]
% zero = meet(X0,complement(X0))
% i.e. zero is the empty relation
%
zero(U1,U2,X,Z) :-
  un(X,M1,cp(U1,U2))
  & disj(X,M1)
  & inters(X,M1,Z).

% top is defined in the axiomatization of relation 
% algebra given in [Hoe08]
% top = join(X0,complement(X0))
% i.e. top is the full relation, i.e. the Cartesian product
top(U1,U2,X,T) :-
  un(X,M1,cp(U1,U2))
  & disj(X,M1)
  & un(X,M1,T).