Algebra Ontology
<![CDATA[
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Functions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defrelation binop (?f ?s) :=
(and (binary-function ?f)
(subset (universe ?f) ?s)))
(defrelation associative (?f ?s) :=
(forall (?x ?y ?z)
(=> (member ?x ?s) (member ?y ?s) (member ?z ?s)
(= (value ?f ?x (value ?f ?y ?z))
(value ?f (value ?f ?x ?y) ?z)))))
(defrelation commutative (?f ?s) :=
(forall (?x ?y)
(=> (member ?x ?s) (member ?y ?s)
(= (value ?f ?x ?y) (value ?f ?y ?x)))))
(defrelation invertible (?f ?o ?s) :=
(forall (?x)
(=> (memberp ?x ?s)
(exists (?y)
(and (member ?y ?s)
(= (value ?x ?y) ?o) (= (value ?y ?x) ?o))))))
(defrelation distributes (?f ?g ?s) :=
(and (binop ?f ?s) (binop ?g ?s)
(forall (?x ?y ?z)
(=> (member ?x ?s) (member ?y ?s) (member ?z ?s)
(= (value ?f (value ?g ?x ?y) ?z)
(value ?g (value ?f ?x ?z) (value ?f ?y ?z)))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Relations
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defrelation binrel (?r ?s) :=
(and (binary-relation ?r)
(subset (universe ?r) ?s)))
(defrelation reflexive (?r ?s) :=
(and (binrel ?r ?s)
(forall (?x) (=> (member ?x ?s) (holds ?r ?x ?x)))))
(defrelation irreflexive (?r ?s) :=
(and (binrel ?r ?s)
(forall (?x) (=> (member ?x ?s) (not (holds ?r ?x ?x))))))
(defrelation symmetric (?r ?s) :=
(and (binrel ?r ?s)
(forall (?x ?y) (=> (holds ?r ?x ?y) (holds ?r ?y ?x)))))
(defrelation asymmetric (?r ?s) :=
(and (binrel ?r ?s)
(forall (?x ?y) (=> (holds ?r ?x ?y)
(not (holds ?r ?y ?x))))))
(defrelation antisymmetric (?r ?s) :=
(and (binrel ?r ?s)
(forall (?x ?y)
(=> (holds ?r ?x ?y) (holds ?r ?y ?x) (= ?x ?y)))))
(defrelation trichotomizes (?r ?s) :=
(and (binrel ?r ?s)
(forall (?x ?y)
(=> (member ?x ?s) (member ?y ?s)
(or (holds ?r ?x ?y) (= ?x ?y) (holds ?r ?y ?x))))))
(defrelation transitive (?r ?s) :=
(and (binrel ?r ?s)
(forall (?x ?y ?z)
(=> (holds ?r ?x ?y) (holds ?r ?y ?z)
(holds ?r ?x ?z)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Algebraic Structures
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defrelation semigroup (?s ?f ?o) :=
(and (binop ?f ?s)
(associative ?f ?s)
(identity ?o ?f ?s)))
(defrelation abelian-semigroup (?s ?f ?o) :=
(and (semigroup ?s ?f ?o)
(commutative ?f ?s)))
(defrelation group (?s ?f ?o) :=
(and (binop ?f ?s)
(associative ?f ?s)
(identity ?o ?f ?s)
(invertible ?f ?o ?s)))
(defrelation abelian-group (?s ?f ?o) :=
(and (group ?s ?f ?o)
(commutative ?f ?s)))
(defrelation ring (?s ?f ?o ?g ?i) :=
(and (abelian-group ?s ?f ?o)
(semigroup ?s ?g ?i)
(distributes ?g ?f ?s)))
(defrelation commutative-ring (?s ?f ?o ?g ?i) :=
(and (abelian-group ?s ?f ?o)
(abelian-semigroup ?s ?g ?i)
(distributes ?g ?f ?s)))
(defrelation integral-domain (?s ?f ?o ?g ?i) :=
(and (commutative-ring ?s ?f ?o ?g ?i)
(operation ?g (difference ?s (setof ?o)))))
(defrelation division-ring (?s ?f ?o ?g ?i) :=
(and (ring ?s ?f ?o ?g ?i)
(binop ?g (difference ?s (setof ?o)))
(invertible ?g (difference ?s (setof ?o)))))
(defrelation field (?s ?f ?o ?g ?i) :=
(and (division-ring ?s ?f ?o ?g ?i)
(commutative ?f ?s)))
;;;;;;;;;;;;;;;;
(defrelation partition (?s ?r) :=
(and (reflexive ?r ?s)
(symmetric ?r ?s)
(transitive ?r ?s)))
(defrelation partial-order (?s ?r) :=
(and (irreflexive ?r ?s)
(asymmetric ?r ?s)
(transitive ?r ?s)))
(defrelation linear-order (?s ?r) :=
(and (irreflexive ?r ?s)
(asymmetric ?r ?s)
(transitive ?r ?s)
(trichotomizes ?r ?s)))
]]>
Michael R. Genesereth