Skip to content
Permalink
Browse files

Merge branch 'master' of https://github.com/gruninger/colore

  • Loading branch information...
jessiezj-li committed Aug 2, 2018
2 parents 0dc332e + 7ae455d commit c1d6e6707fa5fe099be17fe8f4e54dd284acb2c1
Showing 480 changed files with 165,526 additions and 2,311 deletions.
@@ -3,9 +3,26 @@
*.select.tptp
*_nontrivial*
*.DS_Store
*.p9
*.tptp
*.out
.project
*.log
*.aux
*.synctex.gz
*.pyc
*.out
*.bak
*.swp

generated/
output/
conversions/
p9/
output/
provers/
reasoners/
log/

# OS generated files #
######################
@@ -45,9 +62,3 @@ Thumbs.db
*.sql
*.sqlite
ontologies/.DS_Store

.DS_Store
*.p9
*.tptp
*.out
.project
@@ -1,6 +1,6 @@
(cl-text http://colore.oor.net/component/component_def.clif)

(cl-text "Proper Parthood")
(cl-text 'Proper Parthood')
(forall (x y)
(iff (properComponent x y)
(and (componentOf x y)
@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/C-Ext.clif

(cl-comment "C-Ext")
(cl-comment 'C-Ext')

(forall (x y)
(if
@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/C4.clif

(cl-comment "C4")
(cl-comment 'C4')

(forall (x y z)
(if
@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/C5prime.clif

(cl-comment "C5prime")
(cl-comment 'C5prime')

(forall (x z)
(if
@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/Conn.clif

(cl-comment "Con: Connection axiom (connection of an entity with its complement)")
(cl-comment 'Con: Connection axiom (connection of an entity with its complement)')

(forall (x)
(if (and
@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/Dis.clif

(cl-comment "Dis")
(cl-comment 'Dis')

(forall (x)
(if
@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/atomless_boolean_contact_algebra.clif

(cl-comment "atomless Boolean Contact algebra axioms")
(cl-comment 'atomless Boolean Contact algebra axioms')

(cl-imports http://colore.oor.net/contact_algebras/boolean_contact_algebra.clif)

@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/boolean_contact_algebra.clif

(cl-comment "Boolean Contact algebra axioms")
(cl-comment 'Boolean Contact algebra axioms')

(cl-imports http://colore.oor.net/contact_algebras/contact_algebra.clif)

@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/contact_algebra.clif

(cl-comment "axioms of a (pseudocomplemented) contact algebra")
(cl-comment 'axioms of a (pseudocomplemented) contact algebra')

(cl-imports http://colore.oor.net/contact_algebras/distributive_contact_algebra.clif)

@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/distributive_contact_algebra.clif

(cl-comment "Axioms of a distributive contact algebra which satifies the sum axiom C4")
(cl-comment 'Axioms of a distributive contact algebra which satifies the sum axiom C4')

(cl-imports http://colore.oor.net/contact_algebras/weak_contact_algebra.clif)

@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/ewbca.clif

(cl-comment "Extensionsal Weak Boolean Contact algebra axioms (as defined in Hahmann and Gruninger, Notre Dame J. Formal Logic 2013)")
(cl-comment 'Extensionsal Weak Boolean Contact algebra axioms (as defined in Hahmann and Gruninger, Notre Dame J. Formal Logic 2013)')

(cl-imports http://colore.oor.net/contact_algebras/wbca.clif)

@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/extensional_weak_boolean_contact_algebra.clif

(cl-comment "Extensional Weak Boolean Contact algebra axioms")
(cl-comment 'Extensional Weak Boolean Contact algebra axioms')

(cl-imports http://colore.oor.net/contact_algebras/extensional_weak_contact_algebra.clif)

@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/extensional_weak_contact_algebra.clif

(cl-comment "axioms for extensional weak contact algebras")
(cl-comment 'axioms for extensional weak contact algebras')

(cl-imports http://colore.oor.net/contact_algebras/weak_contact_algebra.clif)

@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/gbca.clif

(cl-comment "Generalized Weak Boolean Contact algebra axioms (as defined in Hahmann and Gruninger, Notre Dame J. Formal Logic 2013)")
(cl-comment 'Generalized Weak Boolean Contact algebra axioms (as defined in Hahmann and Gruninger, Notre Dame J. Formal Logic 2013)')

(cl-imports http://colore.oor.net/contact_algebras/wbca.clif)

@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/generalized_boolean_contact_algebra.clif

(cl-comment "Generalized Boolean Contact algebra axioms")
(cl-comment 'Generalized Boolean Contact algebra axioms')

(cl-imports http://colore.oor.net/contact_algebras/contact_algebra.clif)

@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/notC4.clif

(cl-comment "notC4")
(cl-comment 'notC4')

(exists (x y z)
(and
@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/NotTriv.clif

(cl-comment "non-trivial model")
(cl-comment 'non-trivial model')

(exists (y)
(and
@@ -11,7 +11,7 @@

(cl-text http://colore.oor.net/contact_algebras/oca.clif

(cl-comment "equational axiomatization of orthocomplemented contact algebra (as defined in Hahmann and Gruninger, Notre Dame J. Formal Logic 2013)")
(cl-comment 'equational axiomatization of orthocomplemented contact algebra (as defined in Hahmann and Gruninger, Notre Dame J. Formal Logic 2013)')

(cl-imports http://colore.oor.net/contact_algebras/weakest_contact_algebra.clif)

@@ -10,11 +10,11 @@

(cl-text http://colore.oor.net/contact_algebras/proximity_boolean_contact_algebra.clif

(cl-comment "Proximity Boolean Contact algebra (PBCA) axioms")
(cl-comment 'Proximity Boolean Contact algebra (PBCA) axioms')

(cl-imports http://colore.oor.net/contact_algebras/boolean_contact_algebra.clif)

(cl-comment "Nor: Normality axiom ")
(cl-comment 'Nor: Normality axiom ')

(forall (x y)
(if (not (c x y))
@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/region_boolean_contact_algebra.clif

(cl-comment "Region Boolean Contact algebra (RBCA) axioms")
(cl-comment 'Region Boolean Contact algebra (RBCA) axioms')

(cl-imports http://colore.oor.net/contact_algebras/boolean_contact_algebra.clif)

@@ -11,11 +11,11 @@

(cl-text http://colore.oor.net/contact_algebras/spoca.clif

(cl-comment "Stonian p-ortocomplemented contact algebra (as defined in Hahmann and Gruninger, Notre Dame J. Formal Logic 2013)")
(cl-comment 'Stonian p-ortocomplemented contact algebra (as defined in Hahmann and Gruninger, Notre Dame J. Formal Logic 2013)')

(cl-imports http://colore.oor.net/contact_algebras/oca.clif)

(cl-comment "PC1")
(cl-comment 'PC1')

(forall (x y)
(=
@@ -25,15 +25,15 @@
)


(cl-comment "PC2prime")
(cl-comment 'PC2prime')

(= (pc zero) one)

(cl-comment "PC2primeprime")
(cl-comment 'PC2primeprime')

(= (pc one) zero)

(cl-comment "S: Stone property")
(cl-comment 'S: Stone property')

(forall (x y)
(=
@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/wbca.clif

(cl-comment "Weak Boolean Contact algebra axioms (as defined in Hahmann and Gruninger, Notre Dame J. Formal Logic 2013)")
(cl-comment 'Weak Boolean Contact algebra axioms (as defined in Hahmann and Gruninger, Notre Dame J. Formal Logic 2013)')

(cl-imports http://colore.oor.net/contact_algebras/spoca.clif)

@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/weak_boolean_contact_algebra.clif

(cl-comment "Weak Boolean Contact algebra axioms")
(cl-comment 'Weak Boolean Contact algebra axioms')

(cl-imports http://colore.oor.net/contact_algebras/weak_contact_algebra.clif)

@@ -10,7 +10,7 @@

(cl-text http://colore.oor.net/contact_algebras/weak_contact_algebra.clif

(cl-comment "Weak Contact Algebra (WCA, according to Duentsch and Winter 2006: Topological representations of contact lattices)")
(cl-comment 'Weak Contact Algebra (WCA, according to Duentsch and Winter 2006: Topological representations of contact lattices)')

(cl-imports http://colore.oor.net/contact_algebras/weakest_contact_algebra.clif)

@@ -12,24 +12,24 @@

(cl-imports http://colore.oor.net/lattices/bounded_lattice_meet_join.clif)

(cl-comment "C0: Disconnected null region")
(cl-comment 'C0: Disconnected null region')

(forall (x)
(not (c 0 x)))

(cl-comment "C1: Reflexivity")
(cl-comment 'C1: Reflexivity')

(forall (x)
(if (not (= x 0))
(c x x)))

(cl-comment "C2: Symmetry")
(cl-comment 'C2: Symmetry')

(forall (x y)
(if (c x y)
(c y x)))

(cl-comment "C3: Closure (using rewriting of lattice operation leq)")
(cl-comment 'C3: Closure (using rewriting of lattice operation leq)')

(forall (x y z)
(if (and (c x y)
@@ -2,7 +2,7 @@

(cl-imports http://colore.oor.net/containment/containment_def.clif)

(cl-comment "If every object properly contained in x is properly contained in y, x is contained in y.")
(cl-comment 'If every object properly contained in x is properly contained in y, x is contained in y.')

(forall (x y)
(If (exists (z)
@@ -2,7 +2,7 @@

(cl-imports http://colore.oor.net/containment/containment_def.clif)

(cl-comment "no partial overlaps")
(cl-comment 'no partial overlaps')

(forall (x y)
(if (containmentOverlaps x y)
@@ -2,7 +2,7 @@

(cl-imports http://colore.oor.net/containment/containment_def.clif)

(cl-comment "Reflexivity")
(cl-comment 'Reflexivity')

(forall (x)
(containedIn x x)
@@ -2,7 +2,7 @@

(cl-imports http://colore.oor.net/containment/containment_def.clif)

(cl-comment "Transitivity")
(cl-comment 'Transitivity')

(forall (x y z)
(if (and (containedIn x y)
@@ -2,7 +2,7 @@

(cl-imports http://colore.oor.net/containment/containment_def.clif)

(cl-comment "Antisymmetry")
(cl-comment 'Antisymmetry')

(forall (x y)
(if (containedIn x y)
@@ -10,23 +10,23 @@
(region_part r1 r2)))))
)

(cl-comment "Proper Parthood (transitive, irreflexive and asymmetric)")
(cl-comment 'Proper Parthood (transitive, irreflexive and asymmetric)')
(forall (x y)
(iff (properContainedIn x y)
(and (containedIn x y)
(not (x=y))))

)

(cl-comment "Atom")
(cl-comment 'Atom')
(forall (x y)
(iff (AtomicComponent x)
(not (exists (y)
(properContainedIn y x))))

)

(cl-comment "Overlap")
(cl-comment 'Overlap')

(forall (x y)
(iff (containmentOverlaps x y)
@@ -2,7 +2,7 @@
(cl-imports http://colore.oor.net/piece/containment_def.clif)
(cl-imports http://colore.oor.net/piece/piece_def.clif)

(cl-text "Extensionality: Two objects that are not in a containment relationship have at least some uncommon piece. There does not exist any two objects with no uncommon pieces, if the two pieces are all common (shared and identical), which means they share the same spatial area, the same shape, the same size, and the substance/material contained in them are exactly identical, then the two objects are hence identical and can be identified as the same object.")
(cl-text 'Extensionality: Two objects that are not in a containment relationship have at least some uncommon piece. There does not exist any two objects with no uncommon pieces, if the two pieces are all common (shared and identical), which means they share the same spatial area, the same shape, the same size, and the substance/material contained in them are exactly identical, then the two objects are hence identical and can be identified as the same object.')

(forall (x y w)
(if (and (properPieceOf w x)
@@ -1,6 +1,6 @@
(cl-text http://colore.oor.net/duration/date_periodic.clif

(cl-imports http://colore.oor.net/duration/point_duration.clif
(cl-imports http://colore.oor.net/duration/point_duration.clif)

(cl-imports http://colore.oor.net/psl_core/psl_core.clif)

Oops, something went wrong.

0 comments on commit c1d6e67

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