new theories in ringoid and ordered_ringoid

gruninger · Jan 29, 2015 · f67e2ac · f67e2ac
1 parent a6985b9
commit f67e2ac
Show file tree

Hide file tree

Showing 7 changed files with 114 additions and 5 deletions.
diff --git a/ontologies/ordered_ringoid/discrete_ordered_ring.clif b/ontologies/ordered_ringoid/discrete_ordered_ring.clif
@@ -0,0 +1,30 @@
+
+(cl-text http://colore.oor.net/ordered_ringoid/discrete_ordered_ring.clif
+
+(cl-imports http://colore.oor.net/ringoids/ring.clif)
+
+(cl-imports http://colore.oor.net/orderings/linear_ordering.clif)
+
+(cl-imports http://colore.oor.net/orderings/definitions/ordering_defs.clif)
+
+(forall (x y z)
+	(if	(lt x y)
+		(lt (sum x z) (sum y z))))
+
+(forall (x y z)
+	(if	(and	(lt zero x)
+			(lt x y))
+		(lt (prod x z) (prod y z))))
+
+(forall (x y)
+	(if	(lt x y)
+		(exists (z)
+			(= y (sum x z)))))
+
+(lt zero one)
+
+(forall (x)
+	(if	(lt zero x)
+		(leq one x)))
+
+)
diff --git a/ontologies/ordered_ringoid/discrete_ordered_semiring.clif b/ontologies/ordered_ringoid/discrete_ordered_semiring.clif
@@ -0,0 +1,30 @@
+
+(cl-text http://colore.oor.net/ordered_ringoid/discrete_ordered_semiring.clif
+
+(cl-imports http://colore.oor.net/ringoids/semiring.clif)
+
+(cl-imports http://colore.oor.net/orderings/linear_ordering.clif)
+
+(cl-imports http://colore.oor.net/orderings/definitions/ordering_defs.clif)
+
+(forall (x y z)
+	(if	(lt x y)
+		(lt (sum x z) (sum y z))))
+
+(forall (x y z)
+	(if	(and	(lt zero x)
+			(lt x y))
+		(lt (prod x z) (prod y z))))
+
+(forall (x y)
+	(if	(lt x y)
+		(exists (z)
+			(= y (sum x z)))))
+
+(lt zero one)
+
+(forall (x)
+	(if	(lt zero x)
+		(leq one x)))
+
+)
diff --git a/ontologies/ordered_ringoid/euclidean_field.clif b/ontologies/ordered_ringoid/euclidean_field.clif
@@ -1,7 +1,7 @@
 
-(cl-text http://colore.oor.net/ordered_ringoid/euclidean_field
+(cl-text http://colore.oor.net/ordered_ringoid/euclidean_field.clif
 
-(cl-imports http://colore.oor.net/ordered_ringoid/ordered_field)
+(cl-imports http://colore.oor.net/ordered_ringoid/ordered_field.clif)
 
 (forall (x)
 	(if	(leq zero x)

diff --git a/ontologies/ordered_ringoid/ordered_field.clif b/ontologies/ordered_ringoid/ordered_field.clif
@@ -1,9 +1,9 @@
 
-(cl-text http://colore.oor.net/ordered_ringoid/ordered_field
+(cl-text http://colore.oor.net/ordered_ringoid/ordered_field.clif
 
-(cl-imports http://colore.oor.net/ringoids/field)
+(cl-imports http://colore.oor.net/ringoids/field.clif)
 
-(cl-imports http://colore.oor.net/orderings/linear_ordering)
+(cl-imports http://colore.oor.net/orderings/linear_ordering.clif)
 
 (forall (x y z)
 	(if	(leq x y)

diff --git a/ontologies/ringoids/commutative_semiring.clif b/ontologies/ringoids/commutative_semiring.clif
@@ -0,0 +1,9 @@
+
+(cl-text http://colore.oor.net/ringoids/commutative_semiring.clif
+
+(cl-imports http://colore.oor.net/ringoids/semiring.clif)
+
+(forall (x y)
+	(= (prod x y) (prod y x)))
+
+)
diff --git a/ontologies/ringoids/idempotent_semiring.clif b/ontologies/ringoids/idempotent_semiring.clif
@@ -0,0 +1,9 @@
+
+(cl-text http://colore.oor.net/ringoids/idempotent_semiring.clif
+
+(cl-imports http://colore.oor.net/ringoids/semiring.clif)
+
+(forall (x)
+	(= x (sum x x)))
+
+)
diff --git a/ontologies/ringoids/semiring.clif b/ontologies/ringoids/semiring.clif
@@ -0,0 +1,31 @@
+
+(cl-text http://colore.oor.net/ringoids/semiring.clif
+
+(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))))
+
+(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)
+	(and	(= zero (prod zero x))
+		(= zero (prod x zero))))
+
+(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))))
+
+)