%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Reference
%
%    On Some Ternary Relations in Lattices
%    R. Padmanabhan
%    Colloquium Mathematicum 15:195-198, 1966.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

clear(auto_inference).
set(predicate_elim).
set(paramodulation).
set(hyper_resolution).

formulas(sos).

% Lattice Theory

x ^ y = y ^ x                # label("commutativity_meet").
x v y = y v x                # label("commutativity_join").
(x ^ y) ^ z = x ^ (y ^ z)    # label("associativity_meet").
(x v y) v z = x v (y v z)    # label("associativity_join").
(x v y) ^ x = x              # label("absorption_1").
(x ^ y) v x = x              # label("absorption_2").

end_of_list.

formulas(sos).

% Definitions of ternary relations

all xa all xx all xb (A(xa,xx,xb)
    <-> ((xa <= xx & xx <= xb) | (xb <= xx & xx <= xa))).

all xa all xx all xb (B(xa,xx,xb)
    <-> (((xa ^ xx) v (xx ^ xb) = xx) & ((xa v xx) ^ (xx v xb) = xx))).
 
all xa all xx all xb (C(xa,xx,xb)
   <-> ((((xa ^ xx) v (xx ^ xb)) = xx) & ((xa ^ xb) v xx = xx))).

all xa all xx all xb (CS(xa,xx,xb)
   <-> ((((xa v xx) ^ (xx v xb)) = xx) & ((xa v xb) ^ xx = xx))).
 
all xa all xx all xb (D(xa,xx,xb)
   <-> ( ((xa ^ xb) <= xx) & (xx <= (xa v xb)))).

% Definition of less-than-or-equal

all x all y ((x <= y) <-> x ^ y = x).

end_of_list.