Skip to content
Permalink
Browse files

Ringoids: Ring and Semiring updated

  • Loading branch information...
thahmann committed May 1, 2018
1 parent 7d29d2e commit db3007712444114041997a42f5cae6cc2fff0c06
Showing with 57 additions and 35 deletions.
  1. +9 −23 ontologies/ringoids/ring.clif
  2. +48 −12 ontologies/ringoids/semiring.clif
@@ -1,32 +1,18 @@

(cl-text http://colore.oor.net/ringoids/ring.clif

(forall (x y z)
(= (sum (sum x y) z) (sum x (sum y z))))
(cl-imports http://colore.oor.net/ringoids/semiring.clif)

(forall (x)
(and (= x (sum zero x))
(= x (sum x zero))))
(cl-comment 'Existence of an additive inverse')

(forall (x)
(exists (y)
(and (= zero (sum x y))
(= zero (sum y x)))))

(forall (x y)
(= (sum x y) (sum y x)))

(forall (x y z)
(= (prod (prod x y) z) (prod x (prod y z))))

(forall (x)
(and (= x (prod one x))
(= x (prod x one))))

(forall (x y z)
(= (prod x (sum y z)) (sum (prod x y) (prod x z))))

(forall (x y z)
(= (prod (sum x y) z) (sum (prod x z) (prod y z))))
(and
(= zero (sum x y))
(= zero (sum y x))
)
)
)


)
@@ -1,31 +1,67 @@

(cl-text http://colore.oor.net/ringoids/semiring.clif

(cl-comment 'Associativity of sum')

(forall (x y z)
(= (sum (sum x y) z) (sum x (sum y z))))

(forall (x)
(and (= x (sum zero x))
(= x (sum x zero))))

(cl-comment 'Commutativity of sum')

(forall (x y)
(= (sum x y) (sum y x)))


(cl-comment 'Associativity of prod')

(forall (x y z)
(= (prod (prod x y) z) (prod x (prod y z))))

(forall (x)
(and (= x (prod one x))
(= x (prod x one))))

(forall (x)
(and (= zero (prod zero x))
(= zero (prod x zero))))

(cl-comment 'Left distributivity of prod over sum')

(forall (x y z)
(= (prod x (sum y z)) (sum (prod x y) (prod x z))))

(cl-comment 'Right distributivity of prod over sum')

(forall (x y z)
(= (prod (sum x y) z) (sum (prod x z) (prod y z))))

(cl-comment 'zero is identity element for sum')

(forall (x)
(= x (sum zero x))
)

(forall (x)
(= x (sum x zero))
)


(cl-comment 'one is identity element for prod')

(forall (x)
(= x (prod one x))
)

(forall (x)
(= x (prod x one))
)


(cl-comment 'Annihilation by zero (entailed for rings)')

(forall (x)
(= zero (prod zero x))
)

(cl-comment 'Annihilation by zero (entailed for rings)')


(forall (x)
(= zero (prod x zero))
)



)

0 comments on commit db30077

Please sign in to comment.
You can’t perform that action at this time.