NASO_SC_dependence.clif

/*******************************************************************************
 * Copyright (c) University of Toronto and others. All rights reserved. 
 * The content of this file is licensed under the Creative Commons Attribution-
 * ShareAlike 3.0 Unported license. The legal text of this license can be
 * found at http://creativecommons.org/licenses/by-sa/3.0/legalcode.
 *
 * Contributors:
 *    Michael Gruninger, Carmen Chui
 *******************************************************************************/
 
(cl-text NASO_SC_dependence

(cl-comment "Source: WonderWeb Deliverable D18 Ontology Library final by: Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari (2003).")
(cl-comment "Comment: DOLCE axioms from 4.3.7 Dependence and Spatial Dependence")

(cl-comment "Import the DOLCE present theory.")
(cl-imports ../dolce_present)

(cl-comment "Taken directly from HETS axioms - going from sorted logic to unsorted logic.")
(forall (y t)
	(if (SC y)
		(or (not (PRE y t))
			(exists (x)
				(and (NASO x)(PRE x t))))))

(forall (x)
	(if (NASO x)
		(exists (t)
			(PRE x t))))
		
(forall (x t)
	(if (NASO x)
		(if (and (At t)(PRE x t))
			(exists (y)
				(and (SC y)(PRE y t))))))

)