Skip to content
Permalink
Browse files

updated comments in Interval PSL with single quotes

  • Loading branch information...
carmenchui committed Jun 20, 2018
1 parent bf036a7 commit 2de59ed5a027108ee862f25546a6e8e1c3c7e713
@@ -1,37 +1,37 @@
(cl-module ex0715

(cl-comment "Import: theories")
(cl-comment 'Import: theories')
(cl-imports test/interval_psl_core)
(cl-imports test/interval_psl_core2dolce_present)

(cl-comment "================")
(cl-comment "Goal for Prover9")
(cl-comment "================")
(cl-comment '================')
(cl-comment 'Goal for Prover9')
(cl-comment '================')

(cl-comment "modified this axiom and removed Q(x)")
(cl-comment "Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).")
(cl-comment "Identifier: dolce_Td15")
(cl-comment 'modified this axiom and removed Q(x)')
(cl-comment 'Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).')
(cl-comment 'Identifier: dolce_Td15')
(forall (x)
(if (or (ED x)(PD x))
(exists (t)
(PRE x t))))

(cl-comment "Ground Axioms")
(cl-comment 'Ground Axioms')

(cl-comment "Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).")
(cl-comment "Identifier: dolce_Td17")
(cl-comment 'Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).')
(cl-comment 'Identifier: dolce_Td17')
(forall (x t t1)
(if (and (PRE x t)(P t1 t))
(PRE x t1)))

(cl-comment "Source: Foundational Choices in DOLCE by: Stefano Borgo, and Claudio Masolo In: Handbook on Ontologies Springer (2009).")
(cl-comment "Identifier: dolcecore_A7")
(cl-comment 'Source: Foundational Choices in DOLCE by: Stefano Borgo, and Claudio Masolo In: Handbook on Ontologies Springer (2009).')
(cl-comment 'Identifier: dolcecore_A7')
(forall (x t)
(if (PRE x t)(T t)))

(cl-comment "Source: Foundational Choices in DOLCE by: Stefano Borgo, and Claudio Masolo In: Handbook on Ontologies Springer (2009).")
(cl-comment "Identifier: dolcecore_A9")
(cl-comment "Additivity")
(cl-comment 'Source: Foundational Choices in DOLCE by: Stefano Borgo, and Claudio Masolo In: Handbook on Ontologies Springer (2009).')
(cl-comment 'Identifier: dolcecore_A9')
(cl-comment 'Additivity')
(forall (x t t1 t2)
(if (and (PRE x t1)(PRE x t2)(SUM t t1 t2))
(PRE x t)))
@@ -1,39 +1,39 @@
(cl-module ex0717

(cl-comment "Import: theories")
(cl-comment 'Import: theories')
(cl-imports test/interval_mandatory)
(cl-imports test/interval_psl_core2dolce_present)
(cl-imports test/interval_mandatory2dolce_participation)

(cl-comment "Goal for Prover9")
(cl-comment 'Goal for Prover9')

(cl-comment "Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).")
(cl-comment "Identifier: dolce_Ad33")
(cl-comment 'Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).')
(cl-comment 'Identifier: dolce_Ad33')
(forall (x y t)
(if (PC x y t)
(and (ED x)(PD y)(T t))))

(cl-comment "Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).")
(cl-comment "Identifier: dolce_Ad34")
(cl-comment 'Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).')
(cl-comment 'Identifier: dolce_Ad34')
(forall (x t)
(if (and (PD x) (PRE x t))
(exists (y) (PC y x t))))

(cl-comment "Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).")
(cl-comment "Identifier: dolce_Ad35")
(cl-comment 'Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).')
(cl-comment 'Identifier: dolce_Ad35')
(forall (x)
(if (ED x)
(exists (y t) (PC x y t))))

(cl-comment "Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).")
(cl-comment "Identifier: dolce_Ad36")
(cl-comment 'Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).')
(cl-comment 'Identifier: dolce_Ad36')
(forall (x y t)
(if (PC x y t)
(and (PRE x t)(PRE y t))))

(cl-comment "Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).")
(cl-comment "Possibly part of the same module as Ad18? Calls the parthood relation.")
(cl-comment "Identifier: dolce_Ad37")
(cl-comment 'Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).')
(cl-comment 'Possibly part of the same module as Ad18? Calls the parthood relation.')
(cl-comment 'Identifier: dolce_Ad37')
(forall (x y t)
(if (and (ED x)(PD y)(T t))
(iff (PC x y t)
@@ -9,9 +9,9 @@
*******************************************************************************/

(cl-text http://colore.oor.net/interval_psl/interval_mandatory.clif
(cl-comment "Time interval version of mandatory.")
(cl-comment 'Time interval version of mandatory.')

(cl-comment "Import the interval version of PSL-core.")
(cl-comment 'Import the interval version of PSL-core.')
(cl-imports http://colore.oor.net/interval_psl/interval_psl_core.clif)

(cl-imports http://colore.oor.net/psl_core/mandatory.clif)
@@ -9,12 +9,12 @@
*******************************************************************************/

(cl-text http://colore.oor.net/interval_psl/interval_moment.clif
(cl-comment "Time interval version of psl-core with moments.")
(cl-comment 'Time interval version of psl-core with moments.')

(cl-comment "Import the interval version of PSL-core.")
(cl-comment 'Import the interval version of PSL-core.')
(cl-imports http://colore.oor.net/interval_psl/interval_psl_core.clif)

(cl-comment "Import the endpoints version of moments.")
(cl-comment 'Import the endpoints version of moments.')
(cl-imports http://colore.oor.net/combined_time/moment_with_endpoints.clif)

)
@@ -9,39 +9,39 @@
*******************************************************************************/

(cl-text http://colore.oor.net/interval_psl/interval_psl_core.clif
(cl-comment "Time interval version of PSL-CORE.")
(cl-comment 'Time interval version of PSL-CORE.')

(cl-comment "Import the psl-core theory.")
(cl-comment 'Import the psl-core theory.')
(cl-imports http://colore.oor.net/psl_core/psl_core_root.clif)

(cl-comment "Import the Interval with Endpoints theory.")
(cl-comment 'Import the Interval with Endpoints theory.')
(cl-imports http://colore.oor.net/combined_time/interval_with_endpoints.clif)

(cl-comment "Additional axioms that are included in this theory.")
(cl-comment 'Additional axioms that are included in this theory.')

(cl-comment "Source: Michael Gruninger, Carmen Chui.")
(cl-comment "Comment: Indicate that a time interval is not an activity, activity occurrence, object, or timepoint.")
(cl-comment 'Source: Michael Gruninger, Carmen Chui.')
(cl-comment 'Comment: Indicate that a time interval is not an activity, activity occurrence, object, or timepoint.')
(forall (x)
(if (timeinterval x)
(not (or (activity x)
(activity_occurrence x)
(timepoint x)
(object x)))))

(cl-comment "Source: Michael Gruninger, Carmen Chui.")
(cl-comment "Comment: A new relation created to relate a time interval with an activity occurrence or object.")
(cl-comment "Relate a time interval with an activity occurrence and object.")
(cl-comment "psl_interval(x,y)")
(cl-comment 'Source: Michael Gruninger, Carmen Chui.')
(cl-comment 'Comment: A new relation created to relate a time interval with an activity occurrence or object.')
(cl-comment 'Relate a time interval with an activity occurrence and object.')
(cl-comment 'psl_interval(x,y)')
(forall (x y)
(iff (psl_interval x y)
(and (or (activity_occurrence x)(object x))
(timeinterval y)
(= (beginof x)(beginof y))
(= (endof x)(endof y)))))

(cl-comment "Source: Michael Gruninger, Carmen Chui.")
(cl-comment "Comment: A new relation created to relate two intervals together.")
(cl-comment "A time interval z overlays activities x and y.")
(cl-comment 'Source: Michael Gruninger, Carmen Chui.')
(cl-comment 'Comment: A new relation created to relate two intervals together.')
(cl-comment 'A time interval z overlays activities x and y.')
(forall (x y z)
(iff (overlay x y z)
(exists (i1 i2)
@@ -10,9 +10,9 @@

(cl-text interval_mandatory2dolce_participation

(cl-comment "Translation definitions for interval_mandatory into dolce_participates.")
(cl-comment 'Translation definitions for interval_mandatory into dolce_participates.')

(cl-comment "All x and y that participate in z is equivalent to a time interval z that overlays two psl_intervals x and y.")
(cl-comment 'All x and y that participate in z is equivalent to a time interval z that overlays two psl_intervals x and y.')
(forall (x y z t)
(iff (PC x y z)
(and
@@ -24,14 +24,14 @@
(beforeEq t (endof z)))
(participates_in x y t)))))

(cl-comment "The concept of parthood in DOLCE is equivalent to the inclusion of time intervals in Interval PSL Core.")
(cl-comment 'The concept of parthood in DOLCE is equivalent to the inclusion of time intervals in Interval PSL Core.')
(forall (t1 t2)
(iff (P t1 t2)
(and (timeinterval t1)(timeinterval t2)
(beforeEq (beginof t2) (beginof t1))
(beforeEq (endof t1) (endof t2)))))

(cl-comment "Lemmas")
(cl-comment 'Lemmas')

(forall (x)
(if (object x)
@@ -10,38 +10,38 @@

(cl-text interval_psl_core2dolce_present

(cl-comment "Translation definition for interval_psl_core into dolce_present.")
(cl-comment 'Translation definition for interval_psl_core into dolce_present.')

(cl-comment "All endurants in DOLCE are objects in Interval PSL Core.")
(cl-comment 'All endurants in DOLCE are objects in Interval PSL Core.')
(forall (x)
(iff (ED x)(object x)))

(cl-comment "All perdurants in DOLCE are activity occurrences in Interval PSL Core.")
(cl-comment 'All perdurants in DOLCE are activity occurrences in Interval PSL Core.')
(forall (x)
(iff (PD x)(activity_occurrence x)))

(cl-comment "All time intervals in DOLCE are time intervals in Interval PSL Core.")
(cl-comment 'All time intervals in DOLCE are time intervals in Interval PSL Core.')
(forall (x)
(iff (T x)(timeinterval x)))

(cl-comment "The concept of parthood in DOLCE is equivalent to the inclusion of time intervals in Interval PSL Core.")
(cl-comment 'The concept of parthood in DOLCE is equivalent to the inclusion of time intervals in Interval PSL Core.')
(forall (t1 t2)
(iff (P t1 t2)
(and (timeinterval t1)(timeinterval t2)
(beforeEq (beginof t2) (beginof t1))
(beforeEq (endof t1) (endof t2)))))

(cl-comment "The concept of being present in DOLCE is equivalent to the concept of in Interval PSL Core.")
(cl-comment 'The concept of being present in DOLCE is equivalent to the concept of in Interval PSL Core.')
(forall (x y t)
(iff (PRE x t)
(and (or (object x)(activity_occurrence x))
(timeinterval t)
(beforeEq (beginof x)(beginof t))
(beforeEq (endof t)(endof x)))))

(cl-comment "Source: Michael Gruninger, Carmen Chui.")
(cl-comment "Comment: A new relation created to describe the sum of two intervals.")
(cl-comment "A time interval z is the sum of the time intervals of two activities x and y.")
(cl-comment 'Source: Michael Gruninger, Carmen Chui.')
(cl-comment 'Comment: A new relation created to describe the sum of two intervals.')
(cl-comment 'A time interval z is the sum of the time intervals of two activities x and y.')
(forall (x y z)
(iff (SUM z x y)
(and (timeinterval x)
@@ -51,43 +51,43 @@
(and (= (beginof z)(beginof x))(= (endof z)(endof y)))
(and (= (beginof z)(beginof y))(= (endof z)(endof x)))))))

(cl-comment "Lemma")
(cl-comment "Source: Michael Gruninger, Carmen Chui.")
(cl-comment "Comment: For all objects or activity occurrences in PSL, there exists a psl_interval associated with it.")
(cl-comment 'Lemma')
(cl-comment 'Source: Michael Gruninger, Carmen Chui.')
(cl-comment 'Comment: For all objects or activity occurrences in PSL, there exists a psl_interval associated with it.')
(forall (x)
(if (or (object x)(activity_occurrence x))
(exists (t) (psl_interval x t))))

(cl-comment "Lemma")
(cl-comment "Source: Michael Gruninger, Carmen Chui.")
(cl-comment "Comment: Transitivity of the beforeEq axiom.")
(cl-comment 'Lemma')
(cl-comment 'Source: Michael Gruninger, Carmen Chui.')
(cl-comment 'Comment: Transitivity of the beforeEq axiom.')
(forall (x y z)
(if (and (beforeEq x y)(beforeEq y z))
(beforeEq x z)))

(cl-comment "Lemma")
(cl-comment "Source: Michael Gruninger, Carmen Chui.")
(cl-comment "Comment: Transitivity axiom for parthood.")
(cl-comment 'Lemma')
(cl-comment 'Source: Michael Gruninger, Carmen Chui.')
(cl-comment 'Comment: Transitivity axiom for parthood.')
(forall (x y z)
(if (and (P x y)(P y z))
(P x z)))

(cl-comment "Additional axioms that are included in this theory.")
(cl-comment 'Additional axioms that are included in this theory.')

(cl-comment "Source: Michael Gruninger, Carmen Chui.")
(cl-comment "Comment: A new relation created to relate a time interval with an activity occurrence or object.")
(cl-comment "Relate a time interval with an activity occurrence and object.")
(cl-comment "psl_interval(x,y)")
(cl-comment 'Source: Michael Gruninger, Carmen Chui.')
(cl-comment 'Comment: A new relation created to relate a time interval with an activity occurrence or object.')
(cl-comment 'Relate a time interval with an activity occurrence and object.')
(cl-comment 'psl_interval(x,y)')
(forall (x y)
(iff (psl_interval x y)
(and (or (activity_occurrence x)(object x))
(timeinterval y)
(= (beginof x)(beginof y))
(= (endof x)(endof y)))))

(cl-comment "Source: Michael Gruninger, Carmen Chui.")
(cl-comment "Comment: A new relation created to relate two intervals together.")
(cl-comment "A time interval z overlays activities x and y.")
(cl-comment 'Source: Michael Gruninger, Carmen Chui.')
(cl-comment 'Comment: A new relation created to relate two intervals together.')
(cl-comment 'A time interval z overlays activities x and y.')
(forall (x y z)
(iff (overlay x y z)
(exists (i1 i2)

0 comments on commit 2de59ed

Please sign in to comment.
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.