Permalink
Browse files

new lattice theories

  • Loading branch information...
gruninger committed May 28, 2017
1 parent 6fb24be commit bdadf4346977d36bd7071b27f881efcbb1da05ff
@@ -0,0 +1,7 @@
(cl-text http://colore.oor.net/lattices/modular_ortholattice.clif
(cl-imports http://colore.oor.net/lattices/modular_lattice.clif)
(cl-imports http://colore.oor.net/lattices/orthomodular_lattice.clif)
)
@@ -15,16 +15,6 @@
(cl-comment "Pseudocomplemented lattice axioms")
(cl-comment "This section is no longer necessary since pc is a function (clear from the next axiom PC1")
(cl-comment "PC0: Existence of pseudocomplements")
(forall (x)
(exists (y)
(= y (pc x))))
(cl-comment "PC1: Pseudocomplements are meet-complements")
(forall (x)
@@ -35,7 +25,7 @@
(cl-comment "PC2: Behaviour of a pseudocomplement")
(forall (x y)
(if
(iff
(= 0 (meet x y))
(leq y (pc x))
))
@@ -0,0 +1,13 @@
(cl-text http://colore.oor.net/lattices/semicomplemented_lattice.clif
(cl-imports http://colore.oor.net/lattices/bounded_lattice.clif)
(cl-imports http://colore.oor.net/lattices/definitions/lattice_complementation.clif)
(forall (x)
(if (not (= x one))
(exists (y)
(and (not (= zero y))
(= (meet x y))))))
)
@@ -0,0 +1,13 @@
(cl-text http://colore.oor.net/lattices/weak_complemented_lattice.clif
(cl-imports http://colore.oor.net/lattices/bounded_lattice.clif)
(cl-imports http://colore.oor.net/lattices/definitions/lattice_defs.clif)
(forall (x y)
(if (not (leq y x))
(exists (z)
(and (= (meet x z) zero)
(not (= (meet y z) zero))))))
)

0 comments on commit bdadf43

Please sign in to comment.