# definition of boole algebra

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


# definition of and
{?g :gand1 ?a. ?g :gand2 ?b.  ?g :gand3 ?c. ?a :and1 "true". ?b :and2 "true".} log:implies {?c :and3 "true".}.
{?g :gand1 ?a. ?g :gand2 ?b.  ?g :gand3 ?c. ?a :and1 "false". ?b :and2 "true".} log:implies {?c :and3 "false".}.
{?g :gand1 ?a. ?g :gand2 ?b.  ?g :gand3 ?c. ?a :and1 "true". ?b :and2 "false".} log:implies {?c :and3 "false".}.
{?g :gand1 ?a. ?g :gand2 ?b.  ?g :gand3 ?c. ?a :and1 "false". ?b :and2 "false".} log:implies {?c :and3 "false".}.


# definition of or
{?g :gor1 ?a. ?g :gor2 ?b.  ?g :gor3 ?c. ?a :or1 "true". ?b :or2 "true".} log:implies {?c :or3 "true".}.
{?g :gor1 ?a. ?g :gor2 ?b.  ?g :gor3 ?c. ?a :or1 "false". ?b :or2 "true".} log:implies {?c :or3 "true".}.
{?g :gor1 ?a. ?g :gor2 ?b.  ?g :gor3 ?c. ?a :or1 "true". ?b :or2 "false".} log:implies {?c :or3 "true".}.
{?g :gor1 ?a. ?g :gor2 ?b.  ?g :gor3 ?c. ?a :or1 "false". ?b :or2 "false".} log:implies {?c :or3 "false".}.


# definition of not

{?g :gnot1 ?a. ?g :gnot2 ?a1. ?a :not1 "true".} log:implies { ?a1 :not2 "false".}.
{?g :gnot1 ?a. ?g :gnot2 ?a1. ?a :not1 "false".} log:implies { ?a1 :not2 "true".}.

# reciprocity axiom
# this causes loops!!!
#{?a :or ?b, ?c.} log:implies {?a1 :or ?c, ?b.}.
#{?a :and ?b, ?c.} log:implies {?a1 :and ?c, ?b.}.

# associativity axiom

#{?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.}.


#{?a :or ?b,"false".} log:implies {?a :or ?b,?b.}.
#{?a :and ?b,"true".} log:implies {?a :and ?b,?b.}.

#{?b :or ?a, ?na.?na :not ?a. } log:implies {?b :value "true".}.
#{?b :and ?a, ?na.?na :not ?a. } log:implies {?b :value "false".}.

# connection of gates

{?a :oror1 ?a. ?a :or3 ?v.} log:implies {?a :or1 ?v.}.
{?a :oror2 ?a. ?a :and3 ?v.} log:implies {?a :or2 ?v.}. 
{?a :andand1 ?a. ?a :and3 ?v.} log:implies {?a :and1 ?v.}.
{?a :andand2 ?a. ?a :and3 ?v.} log:implies {?a :and2 ?v.}. 
{?a :andnot ?a. ?a :and3 ?v.} log:implies {?a :not1 ?v.}.
{?a :ornot ?a. ?a :or3 ?v.} log:implies {?a :not1 ?v.}.
{?a :notor ?a. ?a :not2 ?v.} log:implies {?a :or3 ?v.}.

#:g1 :gnot1 :a.
#:g1 :gnot2 :a1.
#:a :not1 "true".
#:g2 :gnot1 :a1.
#:g2 :gnot2 :a2.

:g3 :gand1 :a3.
:g3 :gand2 :a4.
:g3 :gand3 :a5.
:a5 :andand1 :a5.
:a3 :and1 "true".
:a4 :and2 "true".
:g4 :gand1 :a5.
:g4 :gand2 :a6.
:g4 :gand3 :a7.
:a6 :and2 "true".
:a7 :andnot :a7.
:g5 :gnot1 :a7.
:g5 :gnot2 :a8.
:g6 :gor1  :a8.
:g6 :gor2  :a9.
:a9 :or2 "false".
:g6 :gor3  :a10.

#:a :and11 "true".
#:b :and12 "true". 
#:carryin :and1 "false".
#:c1 :and13 ?v1.

#:a11 :not :c1.
#:c2 :and :a11,:a.
#:a12 :not :c2.
#:c3 :and :a11,:b.
#:a13 :not :c3.
#:c4 :and :a12,:a13.
#:a14 :not :c4.
#:c5 :and :a14,:carryin.
#:a15 :not :c5.
#:c6 :and :a14,:a15.
#:a16 :not :c6.
#:c7 :and :a15,:carryin.
#:a17 :not :c7.
#:c8 :and :a16,:a17.
#:sum :not :c8.
#:c9 :and :a11,:a15.
#:carryout :not :c9.