# definition of boole algebra

@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <boole#>.


# reciprocity axiom
# reciprocity makes no sense = characteristic of graph: built in the # engine.
#{?a :or ?b, ?c.} log:implies {?a1 :or ?c, ?b.}.
#{?a :and ?b, ?c.} log:implies {?a1 :and ?c, ?b.}.

# associativity axiom
# same remark as for reciprocity: paths are associative.
#{?x :or ?a,?b. ?y :or ?x, ?c. ?z :or ?b, ?c.} log:implies { ?u :or #?a,?z.}.
#{?x :and ?a,?b. ?y :and ?x, ?c. ?z :and ?b, ?c.} log:implies { ?u :and #?a,?z.}.

# distributivity axiom
# y = c and (a or b).   w= (c and a) or (c and b).
#{?x :or ?a, ?b. ?y :and ?c, ?x. ?u :and ?c, ?a. ?v :and ?c,?b.} log:implies {?w :or ?u, #?v.}.
#{?x :and ?a, ?b. ?y :or ?c, ?x. ?u :or ?c, ?a. ?v :or ?c,?b.} log:implies {?w :and ?u, #?v.}.
{?x :or ?a, ?b. ?y :and ?c, ?x. ?u :and ?c, ?a. ?v :and ?c,?b.?w :or ?u, ?v.} log:implies {?w :eq ?y.}.
{?x :and ?a, ?b. ?y :or ?c, ?x. ?u :or ?c, ?a. ?v :or ?c,?b.?w :and ?u, ?v.}log:implies {?x :eq ?w.}.


# unity
{?x :or ?a,"false".}log:implies {?x :eq ?a.}.
{?x :and ?a,"true".}log:implies {?x :eq ?a.}.

# inverse
{?x :not ?y. ?z :or ?x,?y.} log:implies {?z :eq "true".}.
{?x :not ?y. ?z :and ?x,?y.} log:implies {?z :eq "false".}.

:x :or :a, :b.
:y :and :c, :x.   # y = c and (a or b)
:u :and :c, :a.
:v :and :c, :b. 
:w :or :u,:v.   # query: :w :eq :x.  

# idempotentie a and a = a
:x1 :and :a,:a.      # query: :x1 :eq :a.

# de morgan : not(a and b) = (not a or not b)