Permalink
Browse files

added binary psl theories

  • Loading branch information...
michael.gruninger
michael.gruninger committed May 9, 2014
1 parent e8a6e3e commit 22ad0f3af1bf5233bb68f284fd0da325bb99addb
@@ -10,7 +10,7 @@
* note: letter cases preserved in accordance with OWL version
*******************************************************************************/
(cl-text http://colore.oor.net/iswc_events/event.owl.clif
(cl-text http://colore.oor.net/event_ontology/event.clif
(cl-comment 'Thing and Nothing axioms removed 1-20')
@@ -10,7 +10,7 @@
* note: letter cases preserved in accordance with OWL version
*******************************************************************************/
(cl-text http://colore.oor.net/iswc_events/event-x.owl.clif
(cl-text http://colore.oor.net/event_ontology/event_x.clif
(cl-comment 'Thing and Nothing axioms removed 1-20')
(cl-comment 'datatype property axioms removed 21-70')
@@ -10,7 +10,7 @@
* note: letter cases preserved in accordance with OWL version
*******************************************************************************/
(cl-text http://colore.oor.net/iswc_events/lode.owl.clif
(cl-text http://colore.oor.net/lode/lode.clif
(cl-comment 'Thing and Nothing axioms removed 1-14')
@@ -10,7 +10,7 @@
* note: letter cases preserved in accordance with OWL version
*******************************************************************************/
(cl-text http://colore.oor.net/iswc_events/lode-x.owl.clif
(cl-text http://colore.oor.net/lode/lode_x.clif
(cl-comment 'Thing and Nothing axioms removed 1-14')
(cl-comment 'datatype property axioms removed 15-64')
@@ -1,15 +1,7 @@
(cl-text http://colore.oor.net/process_specification_language/psl_outercore.clif
(cl-imports http://colore.oor.net/psl_core/psl_core.clif)
(cl-imports http://colore.oor.net/psl_subactivity/subactivity.clif)
(cl-imports http://colore.oor.net/psl_atomic/atomic.clif)
(cl-imports http://colore.oor.net/psl_occtree/occtree.clif)
(cl-imports http://colore.oor.net/psl_complex/complex.clif)
(cl-imports http://colore.oor.net/psl_disc_state/disc_state.clif)
(cl-imports http://colore.oor.net/psl_actocc/actocc.clif)
@@ -0,0 +1,158 @@
/*******************************************************************************
* Copyright (c) University of Toronto and othersAll rights reserved
* The content of this file is licensed under the Creative Commons Attribution-
* ShareAlike 3.0 Unported licenseThe legal text of this license can be
* found at http://creativecommons.org/licenses/by-sa/3.0/legalcode.
*
* complex_actocc.owl.clif
* Hets generated (and modified) common logic translation of OWL version (for testing expressivity)
* unstructured for easier translation to p9 syntax
* note: letter cases preserved in accordance with OWL version
*******************************************************************************/
(cl-text http://colore.oor.net/psl_actocc/binary_complex_actocc.clif
(cl-imports http://colore.oor.net/psl_atomic/binary_atomic.clif)
(cl-comment 'Thing and Nothing axioms removed')
(cl-comment 'datatype property axioms removed')
(cl-comment 'top and bottom object property axioms removed')
(forall (a) (iff (ArborealSubocc a) (and (Arboreal a)
(exists (b) (and (subactivity_occurrence a
b)
(Activity_Occurrence b))))))
(cl-comment 'Ax1_1')
(forall (a) (iff (LegalSubocc a) (exists (b) (and (subactivity_occurrence a
b)
(Legal b)))))
(cl-comment 'Ax2_2')
(forall (a) (iff (MinimalSubocc a) (and (Activity_Occurrence a)
(not (exists (b) (and (proper_subactivity_occurrence a
b)
(Activity_Occurrence b)))))))
(cl-comment 'Ax3_3')
(forall (a) (iff (NonArboreal a) (and (Activity_Occurrence a)
(not (Arboreal a)))))
(cl-comment 'Ax4_4')
(forall (a) (if (ArborealSubocc a) (Legal a)))
(cl-comment 'Ax5_5')
(forall (a) (if (LegalSubocc a) (Legal a)))
(cl-comment 'Ax6_6')
(forall (a) (if (MinimalSubocc a) (Activity_Occurrence a)))
(cl-comment 'Ax7_7')
(forall (a) (if (NonArboreal a) (Activity_Occurrence a)))
(cl-comment 'Ax8_8')
(forall (a) (if (NonArboreal a) (exists (b) (and (root_occ b
a)
(Arboreal b)))))
(cl-comment 'Ax9_9')
(forall (a) (if (NonArboreal a) (exists (b) (and (subactivity_occurrence b
a)
(Activity_Occurrence b)))))
(cl-comment 'Ax10_10')
(forall (a) (if (Legal a) (MinimalSubocc a)))
(cl-comment 'Ax11_11')
(forall (a) (if (Legal a) (exists (b) (and (root a
b)
(Activity b)))))
(cl-comment 'Ax12_12')
(forall (c
d) (if (proper_subactivity_occurrence c
d) (subactivity_occurrence c
d)))
(cl-comment 'Ax13_13')
(forall (c
d) (if (root_occ c
d) (subactivity_occurrence c
d)))
(cl-comment 'Ax14_14')
(forall (a
b
c) (if (and (root_occ a c)
(root_occ b
c)) (= a b)))
(cl-comment 'Ax15_15')
(forall (a
b
c) (if (and (subactivity_occurrence a
b)
(subactivity_occurrence b
c)) (subactivity_occurrence a
c)))
(cl-comment 'Ax16_16')
(forall (a) (exists (b) (if (atocc a
b) (Activity_Occurrence a))))
(cl-comment 'Ax17_17')
(forall (a) (exists (b) (if (leaf a
b) (Activity_Occurrence a))))
(cl-comment 'Ax18_18')
(forall (a) (exists (b) (if (leaf_occ a
b) (Activity_Occurrence a))))
(cl-comment 'Ax19_19')
(forall (a) (exists (b) (if (root a
b) (Legal a))))
(cl-comment 'Ax20_20')
(forall (a) (exists (b) (if (root_occ a
b) (Legal a))))
(cl-comment 'Ax21_21')
(forall (a) (exists (b) (if (subactivity_occurrence a
b) (Activity_Occurrence a))))
(cl-comment 'Ax22_22')
(forall (b) (exists (a) (if (atocc a
b) (Activity b))))
(cl-comment 'Ax23_23')
(forall (b) (exists (a) (if (leaf a
b) (Activity b))))
(cl-comment 'Ax24_24')
(forall (b) (exists (a) (if (leaf_occ a
b) (Activity_Occurrence b))))
(cl-comment 'Ax25_25')
(forall (b) (exists (a) (if (root a
b) (Activity b))))
(cl-comment 'Ax26_26')
(forall (b) (exists (a) (if (root_occ a
b) (Activity_Occurrence b))))
(cl-comment 'Ax27_27')
(forall (b) (exists (a) (if (subactivity_occurrence a
b) (Activity_Occurrence b))))
(cl-comment 'Ax28_28')
(forall (c
d
e) (if (and (root_occ c e)
(occurrence_of e
d)) (root c
d)))
(cl-comment 'Ax29_29')
)
@@ -0,0 +1,35 @@
/*******************************************************************************
* Copyright (c) University of Toronto and othersAll rights reserved
* The content of this file is licensed under the Creative Commons Attribution-
* ShareAlike 3.0 Unported licenseThe legal text of this license can be
* found at http://creativecommons.org/licenses/by-sa/3.0/legalcode.
*
* atomic.owl.clif
* Hets generated (and modified) common logic translation of OWL version (for testing expressivity)
* unstructured for easier translation to p9 syntax
* note: letter cases preserved in accordance with OWL version
*******************************************************************************/
(cl-text http://colore.oor.net/psl_atomic/binary_atomic.clif
(cl-imports http://colore.oor.net/psl_occtree/binary_occtree.clif)
(cl-imports http://colore.oor.net/psl_subactivity/binary_subactivity.clif)
(cl-comment 'Thing and Nothing axioms removed 1-6')
(cl-comment 'datatype property axioms removed 7-56')
(cl-comment 'top and bottom object property axioms removed')
(forall (a) (if (Atomic a) (Activity a)))
(cl-comment 'Ax1_1')
(forall (a) (if (Generator a) (Atomic a)))
(cl-comment 'Ax2_2')
(forall (a) (if (Primitive a) (Atomic a)))
(cl-comment 'Ax3_3')
)
Oops, something went wrong.

0 comments on commit 22ad0f3

Please sign in to comment.