REL001+0.ax

%------------------------------------------------------------------------------
% File     : REL001+0 : TPTP v7.2.0. Released v3.6.0.
% Domain   : Relation Algebra
% Axioms   : Relation Algebra
% Version  : [Hoe08] axioms.
% English  :

% Refs     : [Mad95] Maddux, R. (1995), Relation-algebraic semantics
%          : [Hoe08] Hoefner (2008), Email to G. Sutcliffe
% Source   : [Hoe08]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of formulae    :   13 (  13 unit)
%            Number of atoms       :   13 (  13 equality)
%            Maximal formula depth :    4 (   3 average)
%            Number of connectives :    0 (   0 ~  ;   0  |;   0  &)
%                                         (   0 <=>;   0 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    1 (   0 propositional; 2-2 arity)
%            Number of functors    :    8 (   3 constant; 0-2 arity)
%            Number of variables   :   25 (   0 singleton;  25 !;   0 ?)
%            Maximal term depth    :    5 (   3 average)
% SPC      : 

% Comments :
%------------------------------------------------------------------------------
%----Definition of Boolean algebra a la Maddux
fof(maddux1_join_commutativity,axiom,(
    ! [X0,X1] : join(X0,X1) = join(X1,X0) )).

fof(maddux2_join_associativity,axiom,(
    ! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )).

fof(maddux3_a_kind_of_de_Morgan,axiom,(
    ! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )).

fof(maddux4_definiton_of_meet,axiom,(
    ! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )).

%----Definition of Sequential Composition
fof(composition_associativity,axiom,(
    ! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )).

fof(composition_identity,axiom,(
    ! [X0] : composition(X0,one) = X0 )).

fof(composition_distributivity,axiom,(
    ! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )).

%----Definition of Converse
fof(converse_idempotence,axiom,(
    ! [X0] : converse(converse(X0)) = X0 )).

fof(converse_additivity,axiom,(
    ! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )).

fof(converse_multiplicativity,axiom,(
    ! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )).

fof(converse_cancellativity,axiom,(
    ! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )).

%---Definition of Identities (greatest and smallest element)
fof(def_top,axiom,(
    ! [X0] : top = join(X0,complement(X0)) )).

fof(def_zero,axiom,(
    ! [X0] : zero = meet(X0,complement(X0)) )).

%------------------------------------------------------------------------------