Permalink
Browse files

corrections to vector spaces and timedurations

  • Loading branch information...
gruninger committed Jan 14, 2016
1 parent 8ba5bea commit 633085a2a95d7b89d03df8361b0b7e6b0e40b7db
Showing with 30 additions and 9 deletions.
  1. +12 −1 ontologies/algebra/module.clif
  2. +16 −6 ontologies/algebra/vectorspace.clif
  3. +2 −2 ontologies/duration/timeduration.clif
@@ -2,15 +2,26 @@
(cl-imports http://colore.oor.net/ringoids/ring.clif)
(cl-imports http://colore.oor.net/magma/abelian_group.clif)
(cl-module ringoid (cl-imports http://colore.oor.net/ringoids/ring.clif))
(cl-module algebra (cl-imports http://colore.oor.net/magma/abelian_group.clif))
(forall (r x y)
(if (and (ringoid r)
(algebra x)
(algebra y))
(= (mult r (op x y)) (op (mult r x) (mult r y))))
(forall (r s x)
(if (and (ringoid r)
(algebra x)
(algebra y))
(= (mult (sum r s) x) (op (mult r x) (mult s x))))
(forall (r s x)
(if (and (ringoid r)
(algebra x)
(algebra y))
(= (mult (prod r s) x) (mult r (mult s x))))
(forall (x)
@@ -1,19 +1,29 @@
(cl-text http://colore.oor.net/algebra/vectorspace.clif
(cl-imports http://colore.oor.net/ringoids/field.clif)
(cl-module ringoid (cl-imports http://colore.oor.net/ringoids/ringoid.clif))
(cl-imports http://colore.oor.net/magma/abelian_group.clif)
(cl-module algebra (cl-imports http://colore.oor.net/magma/abelian_group.clif))
(forall (r x y)
(= (mult r (op x y)) (op (mult r x) (mult r y))))
(if (and (ringoid r)
(algebra x)
(algebra y))
(= (mult r (op x y)) (op (mult r x) (mult r y)))))
(forall (r s x)
(= (mult (sum r s) x) (op (mult r x) (mult s x))))
(if (and (ringoid r)
(algebra x)
(algebra y))
(= (mult (sum r s) x) (op (mult r x) (mult s x)))))
(forall (r s x)
(= (mult (prod r s) x) (mult r (mult s x))))
(if (and (ringoid r)
(algebra x)
(algebra y))
(= (mult (prod r s) x) (mult r (mult s x)))))
(forall (x)
(= x (mult one x)))
(if (algebra x)
(= x (mult one x))))
)
@@ -46,13 +46,13 @@
(if (and (timeduration d)
(field r)
(field s))
(= (mult (add r s) d) (add (mult r d) (mult s d)))))
(= (mult (sum r s) d) (add (mult r d) (mult s d)))))
(forall (d r s)
(if (and (timeduration d)
(field r)
(field s))
(= (mult (mult r s) d) (mult r (mult s d)))))
(= (mult (prod r s) d) (mult r (mult s d)))))
(forall (d)
(if (timeduration d)

0 comments on commit 633085a

Please sign in to comment.