;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; PREFACE ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; This file is a perliminary merge of the SUO ontology sources. The basis for
;; the merge is John Sowa's upper ontology (as described at
;; http://www.bestweb.net/~sowa/ontology/toplevel.htm and in Chapter 2 of his book
;; _Knowledge Representation_, Brooks/Cole, 2000). The definitions and axioms of
;; the other SUO sources have been aligned with this ontology. In addition to Sowa's ontology,
;; the merge incorporates Russell and Norvig's ontology, Casati and Varzi's theory of
;; holes, Allen's temporal axioms, the relatively noncontroversial elements of
;; Smith's and Guarino's respective mereotopologies, and the KIF formalization of the CPR
;; (Core Plan Representation).
;; This ontology uses a first-order modal language, i.e., a first-order language
;; with the sentence operators "nec" (for "necessarily") and "poss" (for "possibly").
;; The ontology contains both primitive and defined constants. Among the primitive
;; predicates are several (e.g., "exists-at") that are borrowed from other ontologies
;; -- moreover, those predicates may be *defined* in those ontologies. Eventually,
;; of course, it will be important to have mechanisms for making such connections
;; explicitly (via, e.g., something like Ontolingua packages).
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; STRUCTURAL ONTOLOGY ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The Structural Ontology consists of definitions (both in the object
;; language and in the metalanguage) of certain syntactic abbreviations that
;; can be both heuristically useful and computationally advantageous.
;;;;;;;;;;;;;;;;;;;;
;; "nth-domain" ;;
;;;;;;;;;;;;;;;;;;;;
;; The "nth-domain" provides a computationally and heuristically
;; convenient mechanism for declaring the intended types of the
;; argument places of a given relation. It cannot be considered a
;; genuine predicate in a standard first-order language as it takes
;; first-order predicates as arguments. Furthermore, it also takes
;; numerals as arguments, which are not part of first-order languages
;; generally. However, it can be understood formally as an
;; abbreviation as follows.
;;
;; Let REL be any n-place predicate, and let M be the numeral for the
;; positive integer m, where m is less than or equal to n. Then we
;; let
;;
;; (nth-domain REL M CLASS)
;;
;; serve as an abbreviation for
;;
;; (forall (VAR_1 ... VAR_n)
;; (=> (REL VAR_1 ... VAR_n)
;; (instance-of VAR_m CLASS)))
;;
;; More generally, let M_1, ..., M_i be the numerals for positive
;; integers m_1, ..., m_i, ordered by size, all less than or equal to
;; n. Then, in general, we let
;;
;; (nth-domain REL M_1 CLASS_1 ... M_i CLASS_i)
;;
;; abbreviate
;;
;; (forall (VAR_1 ... VAR_n)
;; (=> (REL VAR_1 ... VAR_n)
;; (and (instance-of VAR_m_1 CLASS_1)
;; ...
;; (instance-of VAR_m_i CLASS_i))))
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Definite descriptions ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Definite descriptions are not currently part of KIF. However, they
;; are used liberally in this ontology, so an axiom schema -- due
;; largely to Bertrand Russell -- has been introduced to capture its
;; meanings -- roughly, that an object ?x is the A iff A is in fact
;; true of ?x, anything that A is true of must be identical to ?x.
;; So, let WFF be a KIF sentence that contains a single free variable
;; X, and let WFF[Y] be the result of replacing every free occurrence
;; of X in WFF with the variable Y. Then the following is an axiom:
;;
;; (<=> (= X (the (X) WFF))
;; (and WFF
;; (forall (Y)
;; (=> WFF[Y]
;; (= X Y)))))
;;;;;;;;;;;;;;;;
;; "disjoint" ;;
;;;;;;;;;;;;;;;;
(documentation disjoint "Classes X and Y are disjoint iff they share no instances.")
(<=>
(disjoint ?class1 ?class2)
(forall (?X)
(not
(and
(instance-of ?X ?class1)
(instance-of ?X ?class2)))))
;;;;;;;;;;;;;;;;;;;
;; "subclass-of" ;;
;;;;;;;;;;;;;;;;;;;
(documentation subclass-of "X is a subclass of Y only if X and Y are classes, and every instance of X is an instance of Y.")
(forall (?subclass ?class)
(<=> (subclass-of ?subclass ?class)
(and (Class ?subclass)
(Class ?class)
(forall (?x)
(=> (instance-of ?x ?subclass)
(instance-of ?x ?class))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; ONTOLOGY PROPER ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;
;; GENERAL CLASSES ;;
;;;;;;;;;;;;;;;;;;;;;;;;;
;; The following axioms (down to the next comment) represent a simplified version of the tip of
;; Sowa's upper ontology. Concepts in the ontology that were deemed to be of purely
;; philosophical interest are not included here.
(subclass-of Individual Entity)
(subclass-of Relation Entity)
(subclass-of Physical Entity)
(subclass-of Abstract Entity)
(subclass-of Continuant Entity)
(subclass-of Occurrent Entity)
(subclass-of Object Physical)
(subclass-of Object Continuant)
(subclass-of Process Physical)
(subclass-of Process Occurrent)
(subclass-of Schema Abstract)
(subclass-of Schema Continuant)
(subclass-of Script Abstract)
(subclass-of Script Occurrent)
(subclass-of Structure Relation)
(subclass-of Structure Continuant)
(subclass-of Situation Relation)
(subclass-of Situation Occurrent)
;; The following (modified) axioms from Sowa were added to facilitate the merging of the
;; SUO sources.
(subclass-of ContinuousProcess Process)
(subclass-of DiscreteProcess Process)
(subclass-of Act DiscreteProcess)
(subclass-of Sign Relation)
(subclass-of Arrangement Schema)
(subclass-of Attribute Schema)
(subclass-of KineticForm Script)
(subclass-of Procedure Script)
(subclass-of ContinuousObject Object)
(subclass-of CorpuscularObject Object)
(subclass-of HomogeneousObject ContinuousObject)
(subclass-of VariableObject ContinuousObject)
(subclass-of OrganicObject CorpuscularObject)
(subclass-of Assembly CorpuscularObject)
;; The following formulas place 'ChemicalElement', 'Quantity', 'Number', 'Set', and
;; 'Class' itself in the class hierarchy. These concepts are needed to hook several
;; of the Ontolingua ontologies into the upper ontology.
(subclass-of ChemicalElement HomogeneousObject)
(subclass-of TemporalObject HomogeneousObject)
(subclass-of Quantity Arrangement)
(subclass-of Unit-Of-Measure Quantity)
(subclass-of Number Arrangement)
(subclass-of Set Arrangement)
(subclass-of Class Arrangement)
(subclass-of Proposition Arrangement)
;; The following is a reworking of the constants under 'Role' in Sowa's ontology.
(subclass-of Predicate Relation)
(subclass-of Function Relation)
(subclass-of UnaryFunction Function)
(subclass-of BinaryFunction Function)
(subclass-of TernaryFunction Function)
(subclass-of VariableArityFunction Function)
(subclass-of ComponentRelation Predicate)
(instance-of part-of ComponentRelation)
(subclass-of component-of part-of)
(subclass-of external-covering component-of)
(subclass-of internal-component-of component-of)
(instance-of property-of ComponentRelation)
(subclass-of BinaryRelation Predicate)
(subclass-of TernaryRelation Predicate)
(subclass-of VariableArityRelation Predicate)
(subclass-of CaseRole BinaryRelation)
(subclass-of IntentionalRelation BinaryRelation)
(subclass-of PropositionalAttitude IntentionalRelation)
(subclass-of ObjectAttitude IntentionalRelation)
(instance-of stage-of ComponentRelation)
(subclass-of attribute-of property-of)
(subclass-of manner-of property-of)
(instance-of source-of CaseRole)
(instance-of agent CaseRole)
(instance-of recipient CaseRole)
(instance-of beneficiary CaseRole)
(instance-of completion CaseRole)
(instance-of destination CaseRole)
(instance-of duration CaseRole)
(instance-of effector-of CaseRole)
(instance-of experiencer CaseRole)
(instance-of instrument CaseRole)
(instance-of located-at CaseRole)
(instance-of matter CaseRole)
(instance-of medium CaseRole)
(instance-of origin CaseRole)
(instance-of path CaseRole)
(instance-of patient CaseRole)
(instance-of exists-at CaseRole)
(instance-of result CaseRole)
(instance-of theme CaseRole)
;; The following axioms and definitions are taken from Russell & Norvig and from CPR.
;; They have been reformulated in such a way that their content is aligned with Sowa's
;; upper ontology.
(subclass-of Sentence Sign)
(subclass-of Sentence Structure)
(subclass-of Solid Structure)
(subclass-of Liquid Structure)
(subclass-of Gas Structure)
(subclass-of TextObject Sign)
(subclass-of TextObject Structure)
(instance-of containsInformation BinaryRelation)
(nth-domain containsInformation 1 TextObject)
(nth-domain containsInformation 2 Proposition)
(instance-of constraintOfProcedure BinaryRelation)
(nth-domain constraintOfProcedure 1 Procedure)
(nth-domain constraintOfProcedure 2 Requirement)
(instance-of hasAnnotation BinaryRelation)
(nth-domain hasAnnotation 1 Object)
(nth-domain hasAnnotation 2 TextObject)
(instance-of implementsProcedure BinaryRelation)
(nth-domain implementsProcedure 1 Process)
(nth-domain implementsProcedure 2 Procedure)
(instance-of hasPurpose BinaryRelation)
(nth-domain hasPurpose 1 Script)
(nth-domain hasPurpose 2 Schema)
(instance-of subProcedure BinaryRelation)
(nth-domain subProcedure 1 Procedure)
(nth-domain subProcedure 2 Procedure)
(instance-of subPurpose BinaryRelation)
(nth-domain subPurpose 1 Schema)
(nth-domain subPurpose 2 Schema)
(instance-of subProcess BinaryRelation)
(nth-domain subProcess 1 Process)
(nth-domain subProcess 2 Process)
(instance-of standardFor BinaryRelation)
(nth-domain standardFor 1 Standard)
(nth-domain standardFor 2 Object)
(subclass-of Standard Schema)
(subclass-of Requirement Standard)
(subclass-of consumableResource matter)
;; The following definitions of 'AbstractionFn' and 'ExtensionFn', which, respectively,
;; convert classes into their corresponding attributes and vice versa, are suggested by
;; some of Robert E. Kent's work.
(instance-of AbstractionFn UnaryFunction)
(nth-domain AbstractionFn 1 Class)
(range AbstractionFn Attribute)
(instance-of ExtensionFn UnaryFunction)
(nth-domain ExtensionFn 1 Attribute)
(range ExtensionFn Class)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; DOCUMENTATION OF GENERAL CLASSES ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(documentation Abstract "Pure information as distinguished from any particular encoding of the information in a physical medium. Instances of Abstract can be said to exist in the same sense as mathematical objects such as sets and relations, but they cannot exist at a particular place and time without some physical encoding or embodiment.")
(documentation Arrangement "Mathematical structures that do not have spatial dimensions: numbers, sets, lists, algebras, grammars, and the data structures of computer science. All the syntactic forms in natural languages, programming languages, and versions of symbolic logic are included under Arrangement.")
(documentation Assembly "A CorpuscularObject whose discrete parts are completely separable. Whether something is considered an unstructured collection or a structured assembly depends on some agent's intention. A car in working order is a highly structured assembly. But if the parts were disassembled and spread out on some surface, it would be called a collection. Yet if the parts were arranged to spell the word 'CAR', they would again form an assembly, although not one that could be used for transportation. Conversely, if a car were towed to the junk yard, the junk dealer might consider it a collection, even though the parts were in the same order they had been in while it was running.")
(documentation Attribute "Primitive schemas, i.e. schemas that cannot be defined in terms of other schemas. Some examples are: colors, tastes, intensities, etc.")
(documentation CaseRole "The class of predicates relating the spatially distinguished parts of an occurrent. Case roles include the agent, patient or recipient of an action, the flammable substance in a burning process, or the water that falls in rain.")
(documentation ComponentRelation "An umbrella class for any binary relation that relates an Object to an aspect of that object. The three elements of ComponentRelation are part-of, property-of, and stage-of.")
(documentation Continuant "A continuant is an entity whose identity continues to be recognizable over some extended interval of time.")
(documentation ContinuousObject "An entity that is indefinitely divisible to the limits of perception by the available sense organs or measuring instruments.")
(documentation ContinuousProcess "A process in which incremental changes take place continuously. This is the normal kind of physical process.")
(documentation CorpuscularObject "An Object that has separable parts.")
(documentation DiscreteProcess "In a discrete process, which is typical of computer programs or idealized approximations to physical processes, changes occur in discrete steps called events, which are interleaved with periods of inactivity called states.")
(documentation Entity "The universal class of individuals. This is the root node of the ontology.")
(documentation HomogeneousObject "A ContinuousObject in which every part is similar to every other in every relevant respect, e.g., temperature, chemical constitution, density, etc. An example would be a beaker of pure distilled water in a controlled environment.")
(documentation Individual "An entity that can be characterized independently of any relationships it may have to other entities.")
(documentation KineticForm "Includes the information in a reel of motion picture film or the patterns and equations for generating motion in virtual reality.")
(documentation Object "A Physical Continuant which retains its identity over some interval of time. Although no physical entity is ever permanent, an object can have stable properties over its lifespan. The type Object includes ordinary physical objects as well as the instantiations of classes in object-oriented programming languages.")
(documentation Occurrent "An entity that does not have a stable identity during any interval of time. Formally, Occurrent satisfies the following conditions:
* The temporal parts of an occurrent exist at different times.
* The spatial parts of an occurrent may exist at the same time, but an occurrent may have different spatial parts at different times
* There are no identity conditions that can be used to identify two occurrents that are observed in nonoverlapping space-time regions.
A person's lifetime, for example, is an occurrent. Different stages of a life cannot be reliably identified unless some continuant, such as the person's fingerprints or DNA, is recognized by suitable identity conditions at each stage. Even then, the identification depends on an inference that presupposes the uniqueness of the identity conditions.")
(documentation OrganicObject "A CorpuscularObject such as a tree or flower that has parts that are not completely separable, even though there are discontinuities.")
(documentation Physical "An entity that has a location in space-time.")
(documentation Procedure "Any time- or sequence-dependent specification of actions and events: including: computer programs, finite-state machines, Petri nets, robot commands, cooking recipes, musical scores, conference schedules, driving directions, and the scripts of actions and dialog in plays and movies. Although a script is intended to represent a dynamic process, it may have static parts. In a movie film, for example, the sequence of images is a script that determines the motion, but each frame is a schema of a static image.")
(documentation Process "A Physical Occurrent during the interval of interest. Depending on the time scale and level of detail, the same actual entity may be viewed as a stable object or a dynamic process. Even an entity as stable as a diamond could be considered a process when viewed over a long time period or at the atomic level of vibrating particles.")
(documentation Proposition "A subclass of Assembly. In logic, the assertion of a proposition is a claim that the abstraction corresponds to some aspect or configuration of the entity or entities involved. As an example, the statement cat(Yojo) expresses a proposition that Cat characterizes the entity named Yojo.")
(documentation Relation "An entity in a relationship to some other entity.")
(documentation Schema "An Abstract form that has the structure of a Continuant and, thus, does not specify time or timelike relationships. Examples include geometric forms, the syntactic structures of sentences in some language, or the encodings of pictures in a multimedia system.")
(documentation Script "An Abstract form that has the structure of an Occurrent and, thus, represents time sequences. Examples include computer programs, a recipe for baking a cake, a sheet of music to be played on a piano, or a differential equation that governs the evolution of a physical process. A movie can be described by several different kinds of scripts: the first is a specification of the actions and dialog to be acted out by humans; but the sequence of frames in a reel of film is also a script that determines a process carried out by a projector that generates flickering images on a screen.")
(documentation Sign "A Sign is considered as representing something to some agent.")
(documentation Situation "A Relational entity considered as an Occurrent. A situation relates the participants in some process, whose stages may involve different participants at different times.")
(documentation Structure "A Relational entity considered as a Continuant. A structure relates multiple objects whose connections constitute the structure.")
(documentation VariableObject "A ContinuousObject that nonetheless varies in, e.g., temperature, chemical constitution, density, etc. An example would be a large body of water such as the ocean.")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; DOCUMENTATION OF PREDICATES ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(documentation agent "(agent ?ACTION ?AGENT) means that the active animate entity ?AGENT voluntarily initiates ?ACTION. Example: Eve bit an apple.")
(documentation attribute-of "(attribute-of ?ENTITY ?PROPERTY) means that ?PROPERTY is a property of ?ENTITY. Properties include things like colors, shapes, sizes, and weights.")
(documentation beneficiary "(beneficiary ?EVENT ?RECIPIENT) means that ?RECIPIENT derives a benefit from the successful completion of ?EVENT. Example: Diamonds were given to Ruby.")
(documentation completion "(completion ?EVENT ?GOAL) means that ?GOAL is the goal of the temporal process ?EVENT. Example: Mary waited until noon. ")
(documentation component-of "(component-of ?COMPONENT ?WHOLE) means that ?COMPONENT is a piece of ?WHOLE. Examples of pieces include the doors and walls of a house, the states or provinces of a country, or the limbs and organs of an animal.")
(documentation destination "(destination ?EVENT ?GOAL) means that ?GOAL is the goal of the spatial process ?EVENT. Example: Bob went to Danbury.")
(documentation duration "(duration ?EVENT ?TIME) means that the TimeMeasure ?Time is a resource of the temporal process ?EVENT. Example: The truck was serviced for 5 hours.")
(documentation effector-of "(effector-of ?ACTION ?ENTITY) means that ?ENTITY is an active determinant source, either animate or inanimate, that initiates ?ACTION, but without voluntary intention. Example: The tree produced new leaves. ")
(documentation exists-at "exists-at is defined in the PSL temporal ontology, which axiomatizes 'timepoint'. This relation holds between an entity and a timepoint just in case the temporal lifespan of the former includes the latter. The constants located-at and exists-at are spatial and temporal predicates, respectively.")
(documentation experiencer "(experiencer ?EVENT ?ENTITY) means that ?ENTITY is an active animate goal of the experience ?EVENT. Example: Yojo sees the fish.")
(documentation instrument "(instrument ?EVENT ?RESOURCE) means that ?RESOURCE is a resource that is not changed by ?EVENT. Example: The key opened the door.")
(documentation located-at "A very general predicate. (located-at ?X ?Y) means that ?X is situated at ?Y, in some sense. Example: Vehicles arrive at a station. The constants located-at and exists-at are spatial and temporal predicates, respectively.")
(documentation manner-of "(manner-of ?ENTITY ?MANNER) means that the occurent ?ENTITY is qualified by the manner ?MANNER. Manners are usually described by adverbs and include things like the speed of the wind, the style of a dance, or the intensity of a sports competition.")
(documentation matter "(matter ?EVENT ?RESOURCE) means that the resource ?RESOURCE is changed by the event ?EVENT. Example: The gun was carved out of soap.")
(documentation medium "(medium ?EVENT ?RESOURCE) means that ?RESOURCE is a physical resource for the information transfer event ?EVENT. Two examples of such resources are the sound of speech and the electromagnetic signals that transmit data. Example: Bill told Boris by phone.")
(documentation origin "(origin ?EVENT ?SOURCE) means that ?SOURCE is a passive determinant source of the spatial or ambient nexus represented by ?EVENT. Example: The chapter begins on page 20.")
(documentation part-of "(part-of ?PART ?WHOLE) implies that the existence of ?PART is independent of the existence of ?WHOLE.")
(documentation path "(path ?EVENT ?RESOURCE) means that ?RESOURCE is a resource of the spatial nexus ?EVENT. Example: The pizza was shipped via Albany and Buffalo.")
(documentation patient "(patient ?EVENT ?ENTITY) means that ?ENTITY is an essential participant that undergoes some structural change as a result of ?EVENT. Example: The cat swallowed the canary.")
(documentation property-of "The class ComponentRelation has two elements, viz. part-of and property-of. The latter relation holds between an object and something which cannot exist without some substrate. Two subpredicates of property-of are attribute-of and manner-of.")
(documentation recipient "(recipient ?ACTION ?ENTITY) means that ?ENTITY is an animate goal of ?ACTION. Example: Sue sent the gift to Bob.")
(documentation result "(result ?ACTION ?GOAL) means that ?GOAL is an inanimate goal of ?ACTION. Example: Eric built a house.")
(documentation source-of "(source-of ?EVENT ?ENTITY) implies that ?ENTITY is present at the beginning of the process, but need not participate throughout the process.")
(documentation stage-of "The temporally distinguished parts of an occurrent are called stages. In the life of a human being, for example, the stages would include infancy, childhood, adolescence, and adulthood. Other possibly overlapping stages would include education, motherhood, business career, and retirement.")
(documentation theme "(theme ?EVENT ?ENTITY) means that ?ENTITY is an essential participant that may be moved, said, or experienced, but is not structurally changed. Example: Billy likes the Beer.")
;;;;;;;;;;;;;;;;;;;;
;; GENERAL AXIOMS ;;
;;;;;;;;;;;;;;;;;;;;
;; Most of these axioms relate to constants comprising the tip of Sowa's upper ontology.
;; Everything is an entity (due to Robert E. Kent).
(forall (?X) (instance-of ?X Entity))
;; There are entities. (In standard FOPC, this axiom is redundant, since it is implied
;; by the one above. However, it is included here in case a "free logic" or similar,
;; nonstandard interpretation of the ontology is adopted).
(exists (?X) (instance-of ?X Entity))
;; Several variations of the same essential axiom have been proposed. These variations
;; include "Everything is either a class or an entity" (John Sowa) and "Everything is
;; either an individual or a class" (Robert E. Kent). This axiom has not been included
;; here, because it seems very controversial. Where are sets to be located, for example?
;; Another of John Sowa's axioms that have been commented out is: Nothing is both a class
;; and an entity. This seems very controversial, since an adequate ontology is supposed
;; to encompass everything that exists and, presumably, classes exist just as much as sets,
;; numbers, and other mathematical entities that have a place in the ontology.
;;(<=>
;; (instance-of ?x Entity)
;; (not
;; (instance-of ?x Class)))
;; Only entities are instances of classes, and only classes have instances (This is due to both
;; John Sowa and Robert E. Kent).
(=>
(instance-of ?instance ?class)
(and
(instance-of ?instance Entity)
(instance-of ?class Class)))
;; Every class is a subclass of Entity.
(=>
(instance-of ?c Class)
(subclass-of ?c Entity))
;; Abstract is a class.
(instance-of Abstract Class)
;; Something is Abstract just in case it has neither a spatial nor temporal location.
(<=>
(instance-of ?x Abstract)
(and
(not
(exists (?y)
(or
(located-at ?x ?y)
(exists-at ?x ?y))))))
;; Something is Physical just in case it exists at some location at some time.
(<=>
(instance-of ?x Physical)
(exists (?y)
(and
(located-at ?x ?y)
(exists-at ?x ?z))))
;; Abstract and Physical are disjoint.
(disjoint Abstract Physical).
;; A continuant is an object that exists (and, hence, retains its identity) over time,
;; i.e., an object that exists at every point over some interval of time.
(=>
(instance-of ?x Continuant)
(exists (?t1 ?t2)
(and
(instance-of ?t1 TimePoint)
(instance-of ?t2 TimePoint)
(before ?t1 ?t2)
(forall (?t)
(=>
(and
(beforeEq ?t1 t)
(beforeEq t ?t2))
(exists-at ?x ?t))))))
;; Continuant and Occurrent are disjoint.
(disjoint Continuant Occurrent)
;; Each temporal part of an occurrent exists at some timepoint.
;; ISSUE: Can stages (i.e., temporal parts of occurrents) exist at
;; more than one timepoint; in particular, can they they exist across
;; intervals of time?
(=>
(and
(instance-of ?occ Occurrent)
(stage-of ?x ?occ))
(exists (?t)
(exists-at ?x ?t)))
;; Occurrents have temporal parts.
(=>
(instance-of ?occ Occurrent)
(exists (?x)
(stage-of ?x ?occ)))
;; Occurrents have spatial parts.
(=>
(instance-of ?occ Occurrent)
(exists (?x)
(spatial-part-of ?x ?occ)))
;; Individual and Relation are disjoint.
(disjoint Individual Relation)
;; part-of and stage-of cannot be satisfied by the same ordered pair.
(<=>
(part-of ?X ?Y)
(not
(stage-of ?X ?Y)))
;; attribute-of and manner-of cannot be satisfied by the same ordered pair.
(<=>
(attribute-of ?X ?Y)
(not
(manner-of ?X ?Y)))
(disjoint Attribute Manner)
;; The following axiom is from CPR.
(=>
(and
(subAction ?Act1 ?Act2)
(instance-of ?Act1 Action))
(during ?Act1 ?Act2))
;;;;;;;;;;;;;;;;;;;;;;;;;
;; AGENT HIERARCHY ;;
;;;;;;;;;;;;;;;;;;;;;;;;;
;; The following ground facts incorporate the 'Agent' hierarchy from the
;; corresponding ontology on the Ontolingua server.
(subclass-of Agent Object)
(subclass-of Person Agent)
(subclass-of Organization Agent)
(subclass-of Publisher Organization)
(subclass-of University Organization)
(disjoint Person Organization)
(documentation Agent "An agent is something or someone that can act on its
own and produce changes in the world.")
(documentation Organization "An organization is a corporate or similar
institution, distinguished from persons and other agents.")
(documentation University "A university is an institute of higher learning that offers a
graduate research program. Of importance here is the fact that
universities sponsor the publication of dissertations. Any organization
that has been accredited to grant graduate degrees and is recognized
in libraries to be a publisher of dissertations can be called a
university. Some places that call themselves colleges fall under this
category.")
(documentation Publisher "A publisher is an organization that publishes.
The owner of a publishing company may be a person,
and the name of the publisher may be the name of a person.")
;; Axiom defining the class 'Agent' in terms of the case role 'agent'
(<=>
(instance-of ?X Agent)
(exists (?Y)
(agent ?Y ?X)))
;;;;;;;;;;;;;;;;;;;;;;;;;
;; NUMBER HIERARCHY ;;
;;;;;;;;;;;;;;;;;;;;;;;;;
;; The following ground facts incorporate the Number hierarchy from the ontology
;; 'kif-numbers' on the Ontolingua server.
(subclass-of RealNumber Number)
(subclass-of RationalNumber RealNumber)
(subclass-of PositiveRealNumber RealNumber)
(subclass-of NegativeRealNumber RealNumber)
(subclass-of Integer RationalNumber)
(subclass-of EvenInteger Integer)
(subclass-of OddInteger Integer)
(subclass-of NaturalNumber Integer)
(subclass-of NonnegativeInteger Integer)
(subclass-of NegativeInteger Integer)
(subclass-of PositiveInteger Integer)
(subclass-of PositiveNumber Number)
(subclass-of NegativeNumber Number)
(subclass-of ComplexNumber Number)
(valence logBit 2)
(documentation logBit "The formula (logbit ?X ?Y) is true if bit ?Y of ?X is 1.")
(valence logTest 2)
(documentation logTest "The formula (logtest ?X ?Y) is true if the logical and of the two's-complement representation of the integers ?X and ?Y is not zero.")
(instance-of MultiplicationFn VariableArityFunction)
(documentation MultiplicationFn "If ?X, ?Y, ..., ?N denote numbers, then the term
(MultiplicationFn ?X ?Y ... ?N) denotes the product of those numbers.")
(instance-of AdditionFn VariableArityFunction)
(documentation AdditionFn "If ?X, ?Y, ..., ?N are numerical constants, then the term
(AdditionFn ?X ?Y ... ?N) denotes the sum of the numbers corresponding to those
constants.")
(instance-of SubtractionFn VariableArityFunction)
(documentation SubtractionFn "If ?X, ?Y, ..., ?N denote numbers, then the term
(SubtractionFn ?X ?Y ... ?N) denotes the difference between the number denoted
by ?X and the numbers denoted by ?Y through ?N. An exception occurs when ?Y ... ?N = 0,
in which case the term denotes the negation of the number denoted by ?X.")
(instance-of DivisionFn VariableArityFunction)
(documentation DivisionFn "If ?X, ?Y, ..., ?N are numbers, then the term
(DivisionFn ?X ?Y ... ?N) denotes the result ?N obtained by dividing the
number denoted by ?X by the numbers denoted by ?Y through ?N. An exception
occurs when ?Y ... ?N = 1, in which case the term denotes the reciprocal
?X of the number denoted by ?Y ... ?N.")
(instance-of AbsoluteValueFn UnaryFunction)
(documentation AbsoluteValueFn "The term (AbsoluteValueFn ?X) denotes the
absolute value of the object denoted by ?X.")
(instance-of ArcCosineFn UnaryFunction)
(documentation ArcCosineFn "If ?X denotes a number, then the term (ArcCosineFn ?X)
denotes the arc cosine of that number (in radians).")
(instance-of ArithmeticalShiftFn BinaryFunction)
(documentation ArithmeticalShiftFn "The term (ArithmeticalShiftFn ?X ?Y) denotes
the result of arithmetically shifting the object denoted by ?X by the number of
bits denoted by ?Y (left or right shifting depending on the sign of ?Y).")
(instance-of ArcSineFn UnaryFunction)
(documentation ArcSineFn "The term (ArcSineFn ?X) denotes the arc sine of the object
denoted by ?X (in radians).")
(instance-of HyperbolicArcSineFn UnaryFunction)
(documentation HyperbolicArcSine "The term (HyperbolicArcSine ?X) denotes the
hyperbolic arc sine of the object denoted by ?X (in radians).")
(instance-of ArcTangentFn UnaryFunction)
(documentation ArcTangentFn "The term (ArcTangentFn ?X) denotes the arc tangent
of the object denoted by ?X (in radians).")
(instance-of HyperbolicArcTangentFn UnaryFunction)
(documentation HyperbolicArcTangentFn "The term (HyperbolicArcTangent ?X) denotes
the hyperbolic arc tangent of the object denoted by ?X (in radians).")
(instance-of BooleanFn TernaryFunction)
(documentation BooleanFn ""The term (BooleanFn ?OPERATOR ?X ?Y) denotes the
result of applying the operation denoted by ?OPERATOR to the objects
denoted by ?X and ?Y.")
(instance-of CeilingFn UnaryFunction)
(documentation CeilingFn "If ?X denotes a real number, then the term (CeilingFn ?X)
denotes the smallest integer greater than or equal to the anumber denoted by ?X.")
(instance-of ConjugateFn UnaryFunction)
(documentation ConjugateFn "If ?X denotes a complex number, then the term
(ConjugateFn ?X) denotes the complex conjugate of the number denoted by ?X.")
(instance-of CosineFn UnaryFunction)
(documentation CosineFn "The term (CosineFn ?X) denotes the cosine of the object
denoted by ?X (in radians).")
(instance-of HyperbolicCosineFn UnaryFunction)
(documentation HyperbolicCosineFn "The term (HyperbolicCosineFn ?X) denotes the
hyperbolic cosine of the object denoted by ?X (in radians).
(instance-of DecodeFloatFn UnaryFunction)
(documentation DecodeFloatFn "The term (DecodeFloatFn ?X) denotes the mantissa of the
object denoted by ?X.")
(instance-of DenominatorFn UnaryFunction)
(documentation DenominatorFn "The term (DenominatorFn ?X) denotes the denominator
of the canonical reduced form of the object denoted by ?X.")
(instance-of ExponentiationFn BinaryFunction)
(documentation ExponentiationFn "The term (Exponentiation ?X ?Y) denotes ?X raised
to the power of the object denoted by ?Y.")
(instance-of FloatingCeilingFn UnaryFunction)
(documentation FloatingCeilingFn "The term (FloatingCeilingFn ?X) denotes the
smallest integer (as a floating point number) greater than the object denoted by ?X.")
(instance-of FloatingFloorFn UnaryFunction)
(documentation FloatingFloorFn "The term (FloatingFloorFn ?X) denotes the largest
integer (as a floating point number) less than the object denoted by ?X.")
(instance-of FloatingPointNumberFn UnaryFunction)
(documentation FloatingPointNumberFn "The term (FloatingPointNumberFn ?X) denotes
the floating point number equal to the object denoted by ?X.")
(instance-of FloatingDigitFn UnaryFunction)
(range FloatingDigitFn NonnegativeInteger)
(documentation FloatingDigitFn "The term (FloatingDigitFn ?X) denotes the number
of digits used in the representation of a floating point number denoted by ?X.")
(instance-of FloatingPrecisionFn UnaryFunction)
(range FloatingPrecisionFn NonnegativeInteger)
(documentation FloatingPrecisionFn "The term (FloatingPrecisionFn ?X) denotes the
number of significant digits in the floating point number denoted by ?X.")
(instance-of FloatingRadixFn UnaryFunction)
(range FloatingRadixFn NaturalNumber)
(documentation FloatingRadixFn "The term (FloatingRadixFn ?X) denotes the radix
of the floating point number denoted by ?X. The most common values are 2
and 16.")
(instance-of FloatingSignFn BinaryFunction)
(documentation FloatingSignFn "The term (FloatingSignFn ?X ?Y) denotes a
floating-point number with the same sign as the object denoted by ?X and
the same absolute value as the object denoted by ?Y.")
(instance-of FloorFn UnaryFunction)
(range FloorFn Integer)
(documentation FloorFn "The term (FloorFn ?X) denotes the largest integer less
than the object denoted by ?X.")
(instance-of FloatingTruncateFn UnaryFunction)
(documentation FloatingTruncateFn "The term (FloatingTruncateFn ?X)} denotes
the largest integer (as a floating point number) less than the object
denoted by ?X.")
(instance-of GreatestCommonDivisorFn VariableArityFunction)
(documentation GreatestCommonDivisorFn "The term (GreatestCommonDivisorFn ?X ?Y ... ?N)
denotes the greatest common divisor of the objects denoted by ?X through ?N.")
(instance-of ImaginaryPartFn UnaryFunction)
(documentation ImaginaryPartFn "The term (ImaginaryPartFn ?X) denotes the imaginary
part of the object denoted by ?X.")
(instance-of IntegerDecodeFloatFn UnaryFunction)
(range IntegerDecodeFloatFn Integer)
(documentation IntegerDecodeFloatFn "The term (IntegerDecodeFloatFn ?X) denotes
the significand of the object denoted by ?X.")
(instance-of IntegerLengthFn UnaryFunction)
(range IntegerLengthFn NonnegativeInteger)
(documentation IntegerLengthFn "The term (IntegerLengthFn ?X) denotes the
number of bits required to store the absolute magnitude of the object denoted
by ?X.")
(instance-of IntegerSquareRootFn UnaryFunction)
(range IntegerSquareRootFn NonnegativeInteger)
(documentation IntegerSquareRootFn "The term (IntegerSquareRootFn ?X) denotes
the integer square root of the object denoted by ?X.")
(instance-of LeastCommonMultipleFn VariableArityFunction)
(documentation LeastCommonMultipleFn "The term (LeastCommonMultipleFn ?X ?Y ... ?N)
denotes the least common multiple of the objects denoted by ?X, ?Y, ... ?N.")
(instance-of LogFn BinaryFunction)
(documentation LogFn "The term (LogFn ?X ?Y) denotes the logarithm of the
object denoted by ?X in the base denoted by ?Y.")
(instance-of LogicalAndFn VariableArityFunction)
(documentation LogicalAndFn "The term (LogicalAndFn ?X ?Y ... ?N) denotes the
bit-wise logical and of the objects denoted by ?X, ?Y, ... , ?N.")
(instance-of LogicalCountFn UnaryFunction)
(documentation LogicalCountFn "The term (LogicalCountFn ?X) denotes the number
of bits in the object denoted by ?X. If the denotation of ?X is positive, then
the one bits are counted; otherwise, the zero bits in the twos-complement
representation are counted.")
(instance-of LogicalExclusiveOrFn VariableArityFunction)
(documentation LogicalExclusiveOrFn "The term (LogicalExclusiveOrFn ?X ?Y ... ?N)
denotes the logical-exclusive-or of the objects denoted by ?X, ?Y, ..., ?N.")
(instance-of LogicalInclusiveOrBitwiseFn VariableArityFunction)
(documentation LogicalInclusiveOrFn "The term (LogicalInclusiveOrFn ?X ?Y ... ?N)
denotes the bit-wise logical inclusive or of the objects denoted by ?X, ?Y, ... , ?N.
It denotes 0 if there are no arguments.")
(instance-of LogicalNotFn UnaryFunction)
(documentation LogicalNotFn "The term (LogicalNotFn ?X) denotes the bit-wise
logical not of the object denoted by ?X.")
(instance-of LogicalExclusiveOrBitwiseFn VariableArityFunction)
(documentation LogicalExclusiveOrBitwiseFn "The term (LogicalExclusiveOrBitwiseFn ?X ?Y ... ?N) denotes the bit-wise logical exclusive or of the objects denoted by ?X, ?Y, ..., ?N.
It denotes 0 if there are no arguments.")
(instance-of MaxFn VariableArityFunction)
(documentation MaxFn "The term (MaxFn ?X ?Y ... ?N) denotes the largest object
denoted by ?X, ?Y, ... , ?N.")
(instance-of MinFn VariableArityFunction)
(documentation MinFn "The term (MinFn ?X ?Y ... ?N) denotes the smallest object
denoted by ?X, ?Y, ... , ?N.")
(instance-of ModuloFn BinaryFunction)
(documentation ModuloFn "The term (ModuloFn ?X ?Y) denotes the root of the object
denoted by ?X modulo the object denoted by ?Y. The result will have the same sign
as denoted by ?X.")
(instance-of NumeratorFn UnaryFunction)
(documentation NumeratorFn "The term (NumeratorFn ?X) denotes the numerator of the
canonical reduced form of the object denoted by ?X.")
(instance-of PhaseFn UnaryFunction)
(documentation PhaseFn "The term (PhaseFn ?X) denotes the angle part of the polar
representation of the object denoted by ?X (in radians).")
(instance-of Pi-TheNumber RealNumber)
(documentation Pi-TheNumber "Pi-TheNumber is the real number that is the ratio of the perimeter of a circle to its diameter. It is approximately equal to 3.141592653589793.")
(instance-of RationalNumberFn UnaryFunction)
(documentation RationalNumberFn "The term (RationalNumberFn ?X) denotes the rational
representation of the object denoted by ?X.")
(instance-of RealNumberFn UnaryFunction)
(documentation RealNumberFn "The term (RealNumberFn ?X) denotes the real part of the
object denoted by ?X.")
(instance-of RemainderFn BinaryFunction)
(documentation RemainderFn "The term (RemainderFn ?NUMBER ?DIVISOR) denotes the
remainder of the object denoted by ?NUMBER divided by the object denoted by
?DIVISOR. The result has the same sign as the object denoted by ?DIVISOR.")
(instance-of RoundFn UnaryFunction)
(range RoundFn Integer)
(documentation RoundFn "The term (RoundFn ?X) denotes the integer nearest to
the object denoted by ?X. If the object denoted by ?X is halfway between two
integers (for example 3.5), it denotes the nearest integer divisible by 2.")
(instance-of ScaleFloatFn BinaryFunction)
(documentation ScaleFloatFn "The term (ScaleFloatFn ?X ?Y) denotes a floating-point
number that is the representational radix of the object denoted by ?X raised to the
integer denoted by ?Y.")
(instance-of SignumFn UnaryFunction)
(documentation SignumFn "The term (SignumFn ?X) denotes the sign of the object
denoted by ?X. This is one of -1, 1, or 0 for rational numbers and one of
-1.0, 1.0, or 0.0 for floating point numbers.")
(instance-of SineFn UnaryFunction)
(documentation SineFn "The term (SineFn ?X) denotes the sine of the object denoted
by ?X (in radians).")
(instance-of HyperbolicSineFn UnaryFunction)
(documentation HyperbolicSineFn "The term (HyperbolicSineFn ?X) denotes the hyperbolic
sine of the object denoted by ?X (in radians).")
(instance-of SquareRootFn UnaryFunction)
(documentation SquareRootFn "The term (SquareRootFn ?X) denotes the principal
square root of the object denoted by ?X.")
(instance-of TangentFn UnaryFunction)
(documentation TangentFn "The term (TangentFn ?X) denotes the tangent of the
object denoted by ?X (in radians).")
(instance-of HyperbolicTangentFn UnaryFunction)
(documentation HyperbolicTangentFn "The term (HyperbolicTangentFn ?X) denotes
the hyperbolic tangent of the object denoted by ?X (in radians).")
(instance-of TruncateFn UnaryFunction)
(documentation TruncateFn "The term (TruncateFn ?X) denotes the largest integer less
than the object denoted by ?X.")
(instance-of lessThan BinaryRelation)
(documentation lessThan "The formula (lessThan ?X ?Y) is true if and only if
the number denoted by ?X is less than the number denoted by ?Y.")
(instance-of greaterThan BinaryRelation)
(documentation greaterThan "The formula (greaterThan ?X ?Y) is true if and only if
the number denoted by ?X is greater than the number denoted by ?Y.")
(=>
(instance-of ?X EvenInteger)
(= (DivisionFn ?X 2) 0)
(=>
(instance-of ?X OddInteger)
(= (DivisionFn ?X 2) 1)
(<=>
(instance-of ?X NaturalNumber)
(and
(greaterThan ?X 0)
(instance-of ?X Integer)))
(=>
(instance-of ?X NonnegativeInteger)
(or
(greaterThan ?X 0)
(= ?X 0)))
(=>
(instance-of ?X PositiveNumber)
(greaterThan ?X 0))
(=>
(instance-of ?X NegativeNumber)
(greaterThan 0 ?X))
(<=>
(lessThan ?X ?Y)
(greaterThan ?Y ?X))
(<=>
(lessThanOrEqualTo ?X ?Y)
(or
(equal ?X ?Y)
(lessThan ?X ?Y)))
(<=>
(greaterThanOrEqualTo ?X ?Y)
(or
(equal ?X ?Y)
(greaterThan ?X ?Y)))
;;;;;;;;;;;;;;;;;;;;;;;;;
;; UNITS OF MEASURE ;;
;;;;;;;;;;;;;;;;;;;;;;;;;
;; The following formulas incorporate the units of measure in the "Standard Units" ontology on
;; the Ontolingua server.
(subclass-of SystemeInternationalUnit Unit-Of-Measure)
(documentation SystemeInternationalUnit "The class of Systeme International units.")
(subclass-of ElectricalCurrentMeasure Unit-Of-Measure)
(subclass-of MassMeasure Unit-Of-Measure)
(subclass-of LengthMeasure Unit-Of-Measure)
(subclass-of IdentityMeasure Unit-Of-Measure)
(subclass-of InformationMeasure Unit-Of-Measure)
(subclass-of EnergyMeasure Unit-Of-Measure)
(subclass-of LuminosityMeasure Unit-Of-Measure)
(subclass-of TimeMeasure Unit-Of-Measure)
(subclass-of TemperatureMeasure Unit-Of-Measure)
(subclass-of FrequencyMeasure Unit-Of-Measure)
(subclass-of PowerMeasure Unit-Of-Measure)
(subclass-of ResistanceMeasure Unit-Of-Measure)
(subclass-of PressureMeasure Unit-Of-Measure)
(subclass-of ElectricalPotentialMeasure Unit-Of-Measure)
(subclass-of SubstanceMeasure Unit-Of-Measure)
(subclass-of ForceMeasure Unit-Of-Measure)
(subclass-of CurrencyMeasure Unit-Of-Measure)
(instance-of MeasureFn BinaryFunction)
(nth-domain MeasureFn 1 RealNumber)
(nth-domain MeasureFn 2 Unit-Of-Measure)
(documentation MeasureFn "This function maps a real number and a unit of measure to that number of units.")
(instance-of Ampere ElectricalCurrentMeasure)
(instance-of Ampere SystemeInternationalUnit)
(documentation Ampere "SI electrical current unit. It is one of the base units.")
(instance-of Amu MassMeasure)
(documentation Amu "Atomic mass unit, which is the mass of the twelfth part of a the Carbon 12 isotope. ")
(equal
(MeasureFn ?X Amu)
(MeasureFn (MultiplicationFn ?X 1.660434E-24) Gram))
(instance-of Angstrom LengthMeasure)
(equal
(MeasureFn ?X Angstrom)
(MeasureFn (MultiplicationFn ?X 1.0E-10) Meter))
(instance-of AngularDegree IdentityMeasure)
(documentation AngularDegree "Angular measurement unit.")
(equal
(MeasureFn ?X AngularDegree)
(MeasureFn (MultiplicationFn ?X (DivisionFn Pi-TheNumber 180)) Radian))
(instance-of AtomGram MassMeasure)
(Documentation AtomGram "AKA gram-atom. Defined as the mass in grams of a 1 mole of pure substance. For example, 1 atom-gram of Carbon 12 will be 12 grams of pure Carbon 12. 2 atom-grams of the same substance will be 24 grams of it. This is an unusual unit that it is essentially 1 mole of 'stuff' but measured in grams so that the actual value (i.e. mass) depends on the type of substance.")
(instance-of Bit InformationMeasure)
(documentation Bit "One bit of information. A one or a zero.")
(instance-of BritishThermalUnit EnergyMeasure)
(documentation BritishThermalUnit "British thermal unit, a unit of energy.")
(equal
(MeasureFn ?X BritishThermalUnit)
(MeasureFn (MultiplicationFn ?X 1055.0) Joule))
(instance-of Byte InformationMeasure)
(documentation Byte "One byte of information. A byte is eight bits.")
(equal
(MeasureFn ?X Byte)
(MeasureFn (MultiplicationFn ?X 8) Bit))
(instance-of Calorie EnergyMeasure)
(documentation Calorie "A calorie is 4.186 joule.")
(equal
(MeasureFn ?X Calorie)
(MeasureFn (MultiplicationFn ?X 4.186) Joule))
(instance-of Candela LuminosityMeasure)
(instance-of Candela SystemeInternationalUnit)
(documentation Candela "The CANDELA is the SI unit for luminous intensity.")
(instance-of Centimeter LengthMeasure)
(documentation Centimeter "It is the 100th part of a METER")
(equal
(MeasureFn ?X Centimeter)
(MeasureFn (MultiplicationFn ?X 0.01) Meter))
(instance-of Coulomb ElectricalCurrentMeasure)
(instance-of Coulomb SystemeInternationalUnit)
(documentation Coulomb "SI charge unit.")
(equal
(MeasureFn ?X Coulomb)
(PerFn (MeasureFn ?X Ampere) (MeasureFn 1 Second-Duration)))
(instance-of Day-Duration TimeMeasure-Duration)
(documentation Day-Duration "one day, ie 24 hours")
(equal
(MeasureFn ?X Day-Duration)
(MeasureFn (MultiplicationFn ?X 24) Hour-Duration))
(instance-of Degree-Celcius TemperatureMeasure)
(documentation Degree-Celcius "A unit for measuring temperature.
The degree-Kelvin differs from the Celcius scale that the triple point of water is defined to be 273.16 degrees Kelvin while it is 0 degrees Celcius. The magnitudes of intervals in two scales are the same.")
(equal
(MeasureFn ?X Degree-Celcius)
(MeasureFn (SubtractionFn ?X 273.16) Degree-Kelvin))
(instance-of Degree-Kelvin TemperatureMeasure)
(instance-of Degree-Kelvin SystemeInternationalUnit)
(documentation Degree-Kelvin
"A unit of thermodynamic temperature. The degree-Kelvin
differs from the Celcius scale that the triple point of water is defined to be 273.16 degrees Kelvin while it is 0 degrees Celcius. The magnitudes of intervals in two scales are the same.")
(instance-of Degree-Rankine TemperatureMeasure)
(documentation Degree-Rankine
"0 degree Rankine is the same as the absolute zero (i.e. 0 degree Kelvin). The magnitues of a degree Rankine is the same as that of a degree Fahrenheit.")
(equal
(MeasureFn ?X Degree-Rankine)
(MeasureFn (MultiplicationFn ?X 1.8) Degree-Rankine))
(instance-of ElectronVolt EnergyMeasure)
(documentation Electronvolt "The elecronvolt is an energy measure")
(equal
(MeasureFn ?X ElectronVolt)
(MeasureFn (MultiplicationFn ?X 1.6E-19) Joule))
(instance-of Foot LengthMeasure)
(documentation Foot "English length unit of feet.")
(equal
(MeasureFn ?X Foot)
(MeasureFn (MultiplicationFn ?X 0.3048) Meter))
(instance-of Giga-Hertz FrequencyMeasure)
(documentation Giga-Hertz "A unit of measure equal to one billion times per second.")
(equal
(MeasureFn ?X Giga-Hertz)
(MeasureFn (MultiplicationFn ?X 1.0E9) Hertz))
(instance-of Gram MassMeasure)
(documentation Gram "1 kilogram = 1000 Grams")
(equal
(MeasureFn ?X Gram)
(MeasureFn (MultiplicationFn ?X 0.001) Kilogram))
(instance-of Hertz FrequencyMeasure)
(documentation Hertz "A unit of measure equal to a frequency of once per second.")
(equal
(MeasureFn ?X Hertz)
(PerFn (MeasureFn ?X Cycle) (MeasureFn 1 Second)))
(instance-of Hour-Duration TimeMeasure-Duration)
(documentation Hour-Duration "Time unit.")
(equal
(MeasureFn ?X Hour-Duration)
(MeasureFn (MultiplicationFn ?X 60) Minute-Duration))
(instance-of Inch LengthMeasure)
(documentation Inch "English length unit.")
(equal
(MeasureFn ?X Inch)
(MeasureFn (MultiplicationFn ?X 0.0254) Meter))
(instance-of Joule EnergyMeasure)
(instance-of Joule SystemeInternationalUnit)
(documentation Joule "SI energy unit.")
(instance-of Kilo-Byte InformationMeasure)
(documentation Kilo-Byte "One kilo byte (K) of information. One K is 1024 bytes.")
(equal
(MeasureFn ?X Kilo-Byte)
(MeasureFn (MultiplicationFn ?X 1024) Byte))
(instance-of Kilo-Hertz FrequencyMeasure)
(documentation Kilo-Hertz "A unit of measure equal to a frequency of one thousand times per second.")
(equal
(MeasureFn ?X Kilo-Hertz)
(MeasureFn (MultiplicationFn ?X 1000) Hertz))
(instance-of Kilo-Watt PowerMeasure)
(documentation Kilo-Watt "A unit that measures power, ie energy produced or expended per unit of time.")
(equal
(MeasureFn ?X Kilo-Watt)
(MeasureFn (MultiplicationFn ?X 1000) Watt))
(instance-of Kilogram MassMeasure)
(instance-of Kilogram SystemeInternationalUnit)
(documentation Kilogram "The basic unit of mass in the MKS system.")
(equal
(MeasureFn ?X Kilogram)
(MeasureFn (MultiplicationFn ?X 1000) Gram))
(instance-of Kilometer LengthMeasure)
(documentation Kilometer "1 kilometer = 1000 meters")
(equal
(MeasureFn ?X Kilometer)
(MeasureFn (MultiplicationFn ?X 1000) Meter))
(instance-of Mega-Byte InformationMeasure)
(documentation Mega-Byte "One mega byte (MB) of information. One MB is 1024 K.")
(equal
(MeasureFn ?X Mega-Byte)
(MeasureFn (MultiplicationFn ?X 1024) Kilo-Byte))
(instance-of Mega-Hertz FrequencyMeasure)
(documentation Mega-Hertz "A unit of measure equal to one million times per second.")
(equal
(MeasureFn ?X Mega-Hertz)
(MeasureFn (MultiplicationFn ?X 1000) Kilo-Hertz))
(instance-of Mega-Ohm ResistanceMeasure)
(documentation Mega-Ohm "One million ohms.")
(equal
(MeasureFn ?X Mega-Ohm)
(MeasureFn (MultiplicationFn ?X 1.0E6) Ohm))
(instance-of Mega-Pascal PressureMeasure)
(documentation Mega-Pascal " 1 megapascal = 10^6 pascal ")
(equal
(MeasureFn ?X Mega-Pascal)
(MeasureFn (MultiplicationFn ?X 1.0E6) Pascal))
(instance-of Meter LengthMeasure)
(instance-of Meter SystemeInternationalUnit)
(documentation Meter "SI length unit. No conversion function is given because this is a standard.")
(instance-of Micro-Ohm ResistanceMeasure)
(documentation Micro-Ohm "10^(-6) Ohms")
(equal
(MeasureFn ?X Micro-Ohm)
(MeasureFn (MultiplicationFn ?X 0.000001) Ohm))
(instance-of Micro-Volt ElectricalPotentialMeasure)
(documentation Micro-Volt "A unit for measuring electrical potential.")
(equal
(MeasureFn ?X Micro-VoltFn)
(MeasureFn (MultiplicationFn ?X 0.000001) Volt))
(instance-of Mile LengthMeasure)
(documentation Mile "English length unit.")
(equal
(MeasureFn ?X Mile)
(MeasureFn (MultiplicationFn ?X 1609) Meter))
(instance-of Milli-Ampere ElectricalCurrentMeasure)
(documentation Milli-Ampere "A unit of electrical current equal to one thousandth of an ampere.")
(equal
(MeasureFn ?X Milli-Ampere)
(MeasureFn (MultiplicationFn ?X .001) Ampere))
(instance-of Milli-Volt ElectricalPotentialMeasure)
(documentation Milli-Volt "A unit of electrical potential equal to one thousandth of a volt.")
(equal
(MeasureFn ?X Milli-Volt)
(MeasureFn (MultiplicationFn ?X .001) Volt))
(instance-of Minute-Duration TimeMeasure-Duration)
(documentation Minute-Duration "Time unit.")
(instance-of Mole SubstanceMeasure)
(instance-of Mole SystemeInternationalUnit)
(documentation Mole
"SI unit for amount of substance. A mole of a substance is the
amount of that substance that contains 6.02252 x 10^23 elementary
entities. Those entities may be atoms, molecules, ions, electrons,
other particles, or specified groups of such particles. One mole
of carbon atoms (the C^12 isotope) is exactly 12 grams [Halliday
and Resnick]. In this ontology we say that the specified unit
is the molecule, so that the MOLE stands by itself as a unit.")
(instance-of Nano-Ampere ElectricalCurrentMeasure)
(documentation Nano-Ampere "A unit of electrical current equal to one billionth of an ampere.")
(equal
(MeasureFn ?X Nano-Ampere)
(MeasureFn (MultiplicationFn ?X 1.0E-9) Ampere))
(instance-of Nano-Second TimeMeasure-Duration)
(documentation Nano-Second "A unit of measure equal to one trillionth of a second.")
(equal
(MeasureFn ?X Nano-Second)
(MeasureFn (MultiplicationFn ?X 1.0E-9) Second))
(instance-of Newton ForceMeasure)
(instance-of Newton SystemeInternationalUnit)
(documentation Newton "SI force unit.")
(instance-of Ohm ResistanceMeasure)
(documentation Ohm "A unit for measuring electrical resistance.")
(instance-of Pascal PressureMeasure)
(instance-of Pascal SystemeInternationalUnit)
(documentation Pascal "SI pressure unit. Newton/meter^2.")
(instance-of Pico-Ampere ElectricalCurrentMeasure)
(documentation Pico-Ampere "A unit of electrical current equal to one trillionth of an ampere.")
(equal
(MeasureFn ?X Pico-AmpereFn)
(MeasureFn (MultiplicationFn ?X 1.0E-12) Ampere))
(instance-of Pico-Second TimeMeasure-Duration)
(equal
(MeasureFn ?X Pico-Second)
(MeasureFn (Multiplication ?X 1.0E-12) Second-Duration))
(instance-of Pound-Force ForceMeasure)
(documentation Pound-Force "English pound of force.")
(instance-of Pound-Mass MassMeasure)
(documentation Pound-Mass "English pound of mass.")
(equal
(MeasureFn ?X Pound-Mass)
(MeasureFn (MultiplicationFn ?X 0.4536) Kilogram))
(instance-of Radian IdentityMeasure)
(documentation Radian "Angular measurement unit.")
(instance-of Second-Duration TimeMeasure-Duration)
(instance-of Second-Duration SystemeInternationalUnit)
(documentation Second-Duration "The SI standard unit of time.")
(instance-of Slug MassMeasure)
(documentation Slug "English mass unit.")
(equal
(MeasureFn ?X Slug)
(MeasureFn (MultiplicationFn ?X 14.59) Kilogram))
(instance-of Dollar-UnitedStates CurrencyMeasure)
(documentation Dollar-UnitedStates "An example currency unit.")
(instance-of Cent-UnitedStates CurrencyMeasure)
(documentation Cent-UnitedStates "Currency measurement unit.")
(equal
(MeasureFn ?X Cent-UnitedStates)
(MeasureFn (MultiplicationFn ?X .01) Dollar-UnitedStates))
(instance-of Volt ElectricalPotentialMeasure)
(documentation Volt "A unit for measuring electrical potential.")
(instance-of Watt PowerMeasure)
(documentation Watt "A unit that measures power, ie energy produced or expended per unit of time.")
(instance-of Year-Duration TimeMeasure-Duration)
(documentation Year-Duration "one calendar year")
(equal
(MeasureFn ?X Year-Duration)
(MeasureFn (MultiplicationFn ?X 365) Day-Duration))
;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ORGANISM HIERARCHY ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The following formulas incorporate the content in the Natural-Kinds ontology developed by the
;; CNR-ITBM group. This content is essentially a set of high-level biological categories.
(subclass-of Organism OrganicObject)
(subclass-of Plant Organism)
(documentation Plant "An organism having cellulose cell walls, growing by synthesis of inorganic
substances, generally distinguished by the presence of chlorophyll, and lacking the power of locomotion. Plant parts are included here as well.")
(=>
(instance-of ?X Plant)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y CellWall-Peptidoglycan))))
(=>
(instance-of ?X Plant)
(exists (?Y ?Z)
(and
(component-of ?Y ?X)
(instance-of ?Y Pigment)
(result ?Z ?Y)
(instance-of ?Z Photosynthesis))))
(subclass-of Animal Organism)
(documentation Animal "An organism with eukaryotic cells, and lacking stiff cell walls, plastids and photosynthetic pigments. The children of this type in the network are 'Invertebrate', and 'Vertebrate'.")
(disjoint Plant Animal)
(=>
(instance-of ?X Animal)
(exists (?Y ?Z)
(and
(component-of ?X ?Y)
(instance-of ?Y Cell)
(part-of ?Y ?Z)
(instance-of ?Z CellWall-NonRigid))))
(subclass-of Microorganism Organism)
(subclass-of Archaeon Microorganism)
(documentation Archaeon "A member of one of the three domains of life, formerly called Archaebacteria under the taxon Bacteria, but now considered separate and distinct. Archaea are characterized by: 1) the presence of characteristic tRNAs and ribosomal RNAs; 2) the absence of peptidoglycan cell walls; 3) the presence of ether-linked lipids built from branched-chain subunits; and 4) their occurrence in unusual habitats. While archaea resemble bacteria in morphology and genomic organization, they resemble eukarya in their method of genomic replication. Thermoproteales; Methanospirillum; Haloferax volcanii.")
(subclass-of Bacterium Microorganism)
(documentation Bacterium "A small, typically one-celled, prokaryotic micro-organism."))
(=>
(instance-of ?X Bacterium)
(cardinality (setof ?Y (and (component-of ?Y ?X) (instance-of ?Y Cell))) 1))
(=>
(and
(instance-of ?X Bacterium)
(located-at ?X ?Y))
(instance-of ?Y OrganicObject))
(subclass-of Virus Microorganism)
(documentation Virus "An organism consisting of a core of a single nucleic acid enclosed in a
protective coat of protein. A virus may replicate only inside a host living cell. A virus exhibits some but not all of the usual characteristics of living things.")
(=>
(instance-of ?X Virus)
(cardinality (setof ?Y (and (component-of ?Y ?X) (instance-of ?Y Molecule))) 1))
(=>
(instance-of ?X Virus)
(and
(instance-of ?X Nucleic-Acid)
(exists (?Y ?Z)
(and
(external-covering ?Y ?X)
(part-of ?Z ?Y)
(instance-of ?Z Protein)))))
(=>
(and
(instance-of ?X Virus)
(instance-of ?Y Replication)
(effector-of ?Y ?X))
(exists (?Z)
(and
(located-at ?Y ?Z)
(instance-of ?Z Cell))))
(=>
(and
(instance-of ?X Virus)
(located-at ?X ?Y))
(instance-of ?Y OrganicObject))
(subclass-of Chlamydia Microorganism)
(documentation Chlamydia "An organism intermediate in size and complexity between a virus and a bacterium, and which is parasitic within the cells of insects and ticks. Included here are all the chlamydias, also called 'PLT' for psittacosis-lymphogranuloma venereum-trachoma.")
(=>
(instance-of ?X Chlamydia)
(exists (?Y ?Z)
(and
(lives-in ?X ?Y)
(instance-of ?Y Cell)
(component-of ?Y ?Z)
(or
(instance-of ?Z Insect)
(instance-of ?Z Tick)))))
(=>
(and
(instance-of ?X Chlamydia)
(located-at ?X ?Y))
(instance-of ?Y OrganicObject))
(subclass-of Vertebrate Animal)
(documentation Vertebrate "An animal which has a spinal column.")
(=>
(instance-of ?X Vertebrate)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y Spinal-Column))))
(subclass-of Invertebrate Animal)
(disjoint Vertebrate Invertebrate)
(documentation Invertebrate "An animal which has no spinal column. This type has no children
in the network and is assigned to all invertebrate animals.")
(subclass-of Arthropod Invertebrate)
(subclass-of Arachnid Arthropod)
(subclass-of Tick Arachnid)
(subclass-of Insect Arthropod)
(subclass-of Vertebrate-ColdBlooded Vertebrate)
(subclass-of Vertebrate-WarmBlooded Vertebrate)
(disjoint Vertebrate-WarmBlooded Vertebrate-ColdBlooded)
(subclass-of Mammal Vertebrate-WarmBlooded)
(subclass-of Alga Plant)
(documentation Alga "A chiefly aquatic plant that contains chlorophyll, but does not form
embryos during development and lacks vascular tissue.")
(=>
(instance-of ?X Alga)
(exists (?Y)
(and
(lives-in ?X ?Y)
(instance-of ?Y Water))))
(=>
(instance-of ?X Alga)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y Chlorophyll))))
(=>
(instance-of ?X Alga)
(has-developmental-form ?X Incoherent))
(subclass-of Amphibian Vertebrate-ColdBlooded)
(disjoint Amphibian Reptile)
(documentation Amphibian "A cold-blooded, smooth-skinned vertebrate which characteristically hatches as an aquatic larva, breathing by gills. When mature, the amphibian breathes with lungs.")
(=>
(instance-of ?X Amphibian)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y Lungs))))
(=>
(instance-of ?X Amphibian)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y Smooth-Skin))))
(=>
(instance-of ?X Amphibian)
(has-developmental-form ?X Aquatic-Larva))
(subclass-of Bird Vertebrate-WarmBlooded)
(disjoint Bird Mammal)
(documentation Bird "A vertebrate having a constant body temperature and characterized by
the presence of feathers.")
(=>
(instance-of ?X Bird)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y Plumage))))
(subclass-of Fish Vertebrate-ColdBlooded)
(disjoint Fish Reptile)
(documentation Fish "A cold-blooded aquatic vertebrate characterized by fins and breathing by gills. Included here are fishes having either a bony skeleton, such as a perch, or a cartilaginous skeleton, such as a shark, or those lacking a jaw, such as a lamprey or hagfish.")
(=>
(instance-of ?X Fish)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y Gills))))
(=>
(instance-of ?X Fish)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y Fin))))
(=>
(instance-of ?X Fish
(exists (?Y)
(and
(lives-in ?Y ?X)
(instance-of ?Y Water))))
(subclass-of Fungus Plant)
(documentation Fungus "A eukaryotic organism characterized by the absence of chlorophyll and the
presence of a rigid cell wall. Included here are both slime molds and true fungi such as yeasts, molds, mildews, and mushrooms.")
(=>
(instance-of ?X Fungus)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y Cell-Eurkaryotic))))
(=>
(instance-of ?X Fungus)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y CellWall-Rigid))))
(=>
(and
(instance-of ?X Fungus)
(located-at ?X ?Y))
(instance-of ?Y OrganicObject))
(subclass-of Human Mammal)
(documentation Human "Modern man, the only remaining species of the Homo genus. If a term describes a human being from the point of view of occupational, family, social status, etc., then a type from the 'Group' hierarchy is assigned instead.")
(subclass-of Mammal Vertebrate-WarmBlooded)
(documentation Mammal "A vertebrate having a constant body temperature and characterized by the presence of hair, mammary glands and sweat glands.")
(=>
(instance-of ?X Mammal)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y Hair))))
(=>
(instance-of ?X Mammal)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y Mammary-Gland))))
(=>
(instance-of ?X Mammal)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y Sweat-Gland))))
(subclass-of Reptile Vertebrate-ColdBlooded)
(documentation Reptile "A cold-blooded vertebrate having an external covering of scales or horny plates. Reptiles breathe by means of lungs and are generally egg-laying.")
(=>
(instance-of ?X Reptile)
(exists (?Y)
(and
(component-of ?Y ?X)
(instance-of ?Y Lungs))))
(=>
(instance-of ?X Reptile)
(exists (?Y)
(and
(external-covering ?Y ?X)
(or
(instance-of ?Y Scale)
(instance-of ?Y Horny-Plate)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; TEMPORAL DEFINITIONS/AXIOMS ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The first part of this section contains definitions and axioms for 'point in time',
;; 'time interval', and relations between these temporal notions. Most of these definitions
;; and axioms were derived from Allen. The second part of this section is an attempt to
;; incorporate the Simple-Time ontology on the Ontolingua server into the merged ontology.
;; Necessary intermediate constants
(instance-of exists-at BinaryRelation)
(nth-domain exists-at 1 Physical)
(nth-domain exists-at 2 TimePoint)
(documentation exists-at "Means that the Process/Object exists at the given point in time")
(subclass-of TimeInterval TemporalObject)
(documentation TimeInterval "An interval of time.")
(subclass-of TimePoint TemporalObject)
(documentation TimePoint "A TimePoint is not a measurement of time, nor is it a specification of time. It is the point in time. The TimePoints at which events occur can be known with various degrees of precision and approximation, but conceptually TimePoints are point-like and not interval-like. That is, it doesn't make sense to talk about what happens during a TimePoint, or how long the TimePoint lasts.")
(subclass-of TimeMeasure Unit-Of-Measure)
(subclass-of TimeMeasure-Duration TimeMeasure)
(subclass-of TimeMeasure-Position TimeMeasure)
;; Definitions of basic temporal relations
(instance-of BeginFn UnaryFunction)
(nth-domain BeginFn 1 TimeInterval)
(range BeginFn TimePoint)
(documentation BeginFn "A function that maps a time interval to the point of time at which the interval begins")
(instance-of EndFn UnaryFunction)
(nth-domain EndFn 1 TimeInterval)
(range EndFn TimePoint)
(documentation EndFn "A function that maps a time interval to the point of time at which the interval ends")
(instance-of starts BinaryRelation)
(nth-domain starts 1 TimeInterval)
(nth-domain starts 2 TimeInterval)
(documentation starts "Relates one time interval to another time interval with which the first shares the same initial time point and of which the first is a proper part")
;; Axiom specifying the meaning of 'starts'
(<=>
(starts ?t1 ?t2)
(and
(equal
(BeginFn ?t1)
(BeginFn ?t2))
(before
(EndFn ?t1)
(EndFn ?t2))))
;; Definition of 'finishes'
(instance-of finishes BinaryRelation)
(nth-domain finishes 1 TimeInterval)
(nth-domain finishes 2 TimeInterval)
(documentation finishes "Relates one time interval to another time interval with which the first shares the same terminal time point and of which the first is a proper part")
;; Axiom specifying the meaning of 'finishes'
(<=>
(finishes ?t1 ?t2)
(and
(before
(BeginFn ?t2)
(BeginFn ?t1))
(equal
(EndFn ?t2)
(EndFn ?t1))))
;; Note that the definition of 'before' below has been broadened from its statement in Allen.
;; The selectional restrictions for both arguments are now 'TemporalEntity' instead of
;; 'TimeInterval'.
(instance-of before BinaryRelation)
(nth-domain before 1 TemporalEntity)
(nth-domain before 2 TemporalEntity)
(documentation before "Means that the first temporal quantity precedes the second, and there is no overlap between the two quantities")
(not
(before ?t1 ?t1))
(=>
(and
(before ?t1 ?t2)
(before ?t2 ?t3))
(before ?t1 ?t3))
;; Definition of 'beforeEq', from Chris Menzel.
(instance-of beforeEq BinaryRelation)
(nth-domain beforeEq 1 TimePoint)
(nth-domain beforeEq 2 TimePoint)
(documentation beforeEq "Means that the first timepoint either is identical with the second or occurs before it in time")
;; Axiom specifying the full meaning of 'beforeEq'.
(<=>
(beforeEq (?t1 ?t2)
(and
(instance-of ?t1 TimePoint)
(instance-of ?t2 TimePoint)
(or
(before ?t1 ?t2)
(= ?t1 ?t2))))
;; Definition of the relation 'overlaps-TimeInterval-proper'
(instance-of overlaps-TimeInterval-proper BinaryRelation)
(nth-domain overlaps-TimeInterval-proper 1 TimeInterval)
(nth-domain overlaps-TimeInterval-proper 2 TimeInterval)
(documentation overlaps "Means that the first time interval ends after the beginning and before the ending of the second interval")
;; Axiom specifying the meaning of 'overlaps-TimeInterval-proper'
(<=>
(overlaps-TimeInterval-proper ?t1 ?t2)
(and
(before
(BeginFn ?t2)
(BeginFn ?t1)
(before
(BeginFn ?t2)
(EndFn ?t1))
(before
(EndFn ?t1)
(EndFn ?t2))))
;; Definition and axiom for 'overlaps-TimeInterval-general'. Note that this relation was
;; extracted from Russell-Norvig's ontology.
(instance-of overlaps-TimeInterval-general BinaryRelation)
(nth-domain overlaps-TimeInterval-general 1 TimeInterval)
(nth-domain overlaps-TimeInterval-general 2 TimeInterval)
(documentation overlaps-TimeInterval-general "Means that the two time intervals have some time interval in common")
(<=>
(overlaps-TimeInterval-general ?t1 ?t2)
(and
(exists ?t3
(and
(during ?t3 ?t1)
(during ?t3 ?t2)))))
;; Definition of the relation 'meets'
(instance-of meets BinaryRelation)
(nth-domain meets 1 TimeInterval)
(nth-domain meets 2 TimeInterval)
(documentation meets "Means that the terminal point of the first interval is the initial point of the second interval")
;; Axiom specifying the meaning of 'meets'
(<=>
(meets ?t1 ?t2)
(equal
(EndFn ?t1)
(BeginFn ?t2)))
;; Extensionality Axiom for 'equal'
(=>
(and
(equal
(BeginFn ?t1)
(BeginFn ?t2))
(equal
(EndFn ?t1)
(EndFn ?t2)))
(equal ?t1 ?t2))
;; Definition of 'during'
(instance-of during BinaryRelation)
(nth-domain during 1 TimeInterval)
(nth-domain during 2 TimeInterval)
(documentation during "Means that the first time interval starts after and ends before the second time interval")
;; Axiom specifying the meaning of 'during'
(=>
(during ?t1 ?t2)
(and
(endof ?t1 ?e1)
(endof ?t2 ?e2)
(lessThan ?e1 ?e2)
(startof ?t1 ?s1)
(startof ?t2 ?s2)
(greaterThan ?s1 ?s2)))))
;; Definition of 'in-TimeInterval'
(instance-of in-TimeInterval BinaryRelation)
(nth-domain in-TimeInterval 1 TimeInterval)
(nth-domain in-TimeInterval 2 TimeInterval)
(documentation in-TimeInterval "Means that the first time interval is a proper part of the second time interval")
(<=>
(in-TimeInterval ?t1 ?t2)
(or
(during ?t1 ?t2)
(starts ?t1 ?t2)
(finishes ?t1 ?t2)))
;; Axiom concerning 'meets', 'during', and 'overlaps'
(=>
(and
(meets ?t1 ?t2)
(during ?t2 ?t3))
(or
(overlaps ?t1 ?t3)
(during ?t1 ?t3)
(meets ?t1 ?t3)))
;; The following definitions and axioms (down to the next section break) cover the content in
;; the Simple-Time ontology on the Ontolingua server.
(instance-of time BinaryRelation)
(nth-domain time 1 DiscreteProcess)
(nth-domain time 2 TimeMeasure-Position)
(documentation time "A general relation that specifies, at any level of resolution, the time at which a particular event occurs.")
(instance-of date BinaryRelation)
(nth-domain date 1 DiscreteProcess)
(nth-domain date 2 Day)
(subclass-of date time)
(documentation date "A binary relation that specifies a point in absolute calendar time, at the
resolution of one day, for a particular event.")
(instance-of YearFn UnaryFunction)
(nth-domain YearFn 1 NaturalNumber)
(range YearFn Year)
(documentation YearFn "A unary function that maps a number to the corresponding calendar year.")
(instance-of MonthFn BinaryFunction)
(nth-domain MonthFn 1 NaturalNumber)
(nth-domain MonthFn 2 Year)
(range MonthFn Month)
(documentation MonthFn "A binary function that maps a number and a year to the corresponding month of the year.")
(instance-of DayFn BinaryFunction)
(nth-domain DayFn 1 NaturalNumber)
(nth-domain DayFn 2 Month)
(range DayFn Day)
(documentation DayFn "A binary function that maps a number and a month to the corresponding day of the month.")
(instance-of HourFn BinaryFunction)
(nth-domain HourFn 1 PositiveRealNumber)
(nth-domain HourFn 2 Day)
(range HourFn "A binary function that maps a number and a day to the corresponding hour of the day.")
(instance-of MinuteFn BinaryFunction)
(nth-domain MinuteFn 1 PositiveRealNumber)
(nth-domain MinuteFn 2 Hour)
(range MinuteFn Minute)
(documentation MinuteFn "A binary function that maps a number and a hour to the corresponding minute of the hour.")
(instance-of SecondFn BinaryFunction)
(nth-domain SecondFn 1 PositiveRealNumber)
(nth-domain SecondFn 2 Minute)
(range SecondFn Second)
(documentation SecondFn "A binary function that maps a number and a minute to the corresponding second of the minute.")
(subclass-of Year TimeMeasure-Position)
(subclass-of Month TimeMeasure-Position)
(=>
(instance-of (MonthFn ?X ?Y) Month)
(lessThanOrEqualTo ?X 12))
(subclass-of Day TimeMeasure-Position)
(=>
(instance-of (DayFn ?X ?Y) Day)
(lessThanOrEqualTo ?X 31))
(subclass-of Hour TimeMeasure-Position)
(=>
(instance-of (HourFn ?X ?Y) Hour)
(lessThanOrEqualTo ?X 24))
(subclass-of Minute TimeMeasure-Position)
(=>
(instance-of (MinuteFn ?X ?Y) Minute)
(lessThanOrEqualTo ?X 60))
(subclass-of Second TimeMeasure-Position)
(=>
(instance-of (SecondFn ?X ?Y) Second)
(lessThanOrEqualTo ?X 60))
(<=>
(instance-of ?X BinaryRelation)
(valence ?X 2))
(<=>
(instance-of ?X TernaryRelation)
(valence ?X 3))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; MEREOTOPOLOGICAL DEFINITIONS/AXIOMS ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Most of this content is taken from Barry Smith's and Nicola Guarino's papers.
;; Definition of 'part-of'
(instance-of part-of BinaryRelation)
(nth-domain part-of 1 CorpuscularObject)
(nth-domain part-of 2 CorpuscularObject)
(documentation part-of "The primitive mereological relation. All other mereological relations are defined in terms of this.")
;; Axiom about the extensionality of 'part-of' from Smith and Sowa
(=>
(forall (?Z)
(=>
(part-of ?Z ?X)
(overlaps ?Z ?Y))
(part-of ?X ?Y))
;; Reflexivity, Antisymmetry, and Transitivity of 'part-of' from Smith
(part-of ?X ?X)
(=>
(and
(part-of ?X ?Y)
(part-of ?Y ?X))
(= ?X ?Y))
(=>
(and
(part-of ?X ?Y)
(part-of ?Y ?Z))
(part-of ?X ?Z))
;; Axiom relating 'part-of' and 'equal'
(=>
(and
(part-of ?X ?Y)
(part-of ?Y ?X))
(equal ?X ?Y))
;; Definition of 'overlaps'
(instance-of overlaps BinaryRelation)
(nth-domain overlaps 1 CorpuscularObject)
(nth-domain overlaps 2 CorpuscularObject)
(documentation overlaps "?x overlaps ?y iff ?x and ?y have some parts in common. This is a reflexive and symmetric (but not transitive) relation.")
;; Axiom specifying the meaning of 'overlaps' (from Guarino)
(<=>
(overlaps ?X ?Y)
(exists (?Z)
(and
(part-of ?Z ?X)
(part-of ?Z ?Y))))
;; Definition of 'proper-part-of'
(subclass-of proper-part-of part-of)
(documentation proper-part-of "?x is a proper part of ?y iff ?x is a part of ?y other than ?y itself. This is a transitive and asymmetric (hence irreflexive) relation.")
;; Axiom specifying part of the meaning of 'proper-part-of' (from Smith)
(<=>
(proper-part-of ?X ?Y)
(and
(part-of ?X ?Y)
(not
(part-of ?Y ?X))))
;; Definition of 'proper-overlaps'
(subclass-of proper-overlaps overlaps)
;; Axiom specifying part of the meaning of 'proper-overlaps' (from Guarino)
(=>
(proper-overlaps ?X ?Y)
(and
(not
(part-of ?X ?Y))
(not
(part-of ?Y ?X))))
;; Definition of 'interior-part-of'
(subclass-of interior-part-of part-of)
;; Axiom specifying part of the meaning of 'interior-part-of' (from Smith)
(=>
(interior-part-of ?X ?Y)
(forall (?Z)
(=>
(boundary ?Z ?Y)
(not
(overlaps ?X ?Z)))))
;; Definition of 'superficial-part-of' (from Casati and Varzi)
(subclass-of superficial-part-of part-of)
(documentation superficial-part-of "?x is a superficial part of ?y iff ?x is a part of ?y that has no interior parts of its own (or, intuitively, that only overlaps those parts of y that are externally connected with the geometric complement of y). This too is a transitive relation closed under sum-of and prod-of.")
;; Axiom specifying part of the meaning of 'superficial-part-of' (from Casati and Varzi)
(=>
(superficial-part-of ?x ?y)
(not
(exists (?z)
(interior-part-of ?z ?x)))))
;; Definition of 'surface-of' (from Casati and Varzi)
(subclass-of surface-of superficial-part-of)
(documentation surface-of "?x is a surface of ?y iff ?x is a maximally connected superficial part of y.")
;; Axiom specifying part of the meaning of 'surface-of' (from Casati and Varzi)
(=>
(surface-of ?x ?y)
(and
(self-connected ?x)
(forall (?z)
(=>
(and
(superficial-part-of ?z ?y)
(self-connected ?z))
(=>
(connected-to ?z ?x)
(part-of ?z ?x)))))))
;; Definitions and Axioms for the notions of mereological sum, product, and difference.
(instance-of MereologicalFn BinaryFunction)
(nth-domain MereologicalFn 1 CorpuscularObject)
(nth-domain MereologicalFn 2 CorpuscularObject)
(documentation MereologicalFn "This is an umbrella relation for MereologicalSumFn, MereologicalProductFn, and MereologicalDifferenceFn.")
(subclass-of MereologicalSumFn MereologicalFn)
(equal
(MereologicalSumFn ?X ?Y)
(the (?Z)
(forall (?W)
(<=>
(overlaps ?W ?Z)
(or
(overlaps ?W ?X)
(overlaps ?W ?Y))))))
(subclass-of MereologicalProductFn MereologicalFn)
(equal
(MereologicalProductFn ?X ?Y)
(the (?Z)
(forall (?W)
(<=>
(part-of ?W ?Z)
(and
(part-of ?W ?X)
(part-of ?W ?Y))))))
(subclass-of MereologicalDifferenceFn MereologicalFn)
(equal
(MereologicalDifferenceFn ?X ?Y)
(the (?Z)
(forall (?W)
(<=>
(part-of ?W ?Z)
(and
(part-of ?W ?X)
(not
(overlaps ?W ?Y)))))))
;; Definition of 'MaximalBoundaryFn'
(instance-of MaximalBoundaryFn UnaryFunction)
(nth-domain MaximalBoundaryFn 1 CorpuscularObject)
(range MaximalBoundaryFn CorpuscularObject)
(equal
(MaximalBoundaryFn ?X)
(the (?Z)
(forall (?W)
(=>
(boundary ?W ?X)
(part-of ?W ?Z)))))
;; Definition of 'ClosureFn' (of an object)
(equal
(ClosureFn ?X)
(MereologicalSumFn ?X (MaximalBoundaryFn ?X)))
;; Basic axioms for a topology based on bona fide boundaries - these are the result
;; of mereologizing the standard Kuratowski axioms for closure operators
(part-of ?X (ClosureFn ?X))
(part-of (ClosureFn (ClosureFn ?X)) (ClosureFn ?X))
(=
(ClosureFn (MereologicalSumFn ?X ?Y))
(MereologicalSumFn (ClosureFn ?X) (ClosureFn ?Y)))
;; Definition of the relation of 'connected' from Smith
(instance-of connected BinaryRelation)
(nth-domain connected 1 CorpuscularObject)
(nth-domain connected 2 CorpuscularObject)
(<=>
(connected ?X ?Y)
(overlaps (ClosureFn ?X) (ClosureFn ?Y)))
;; Definition of 'externally-connected' (i.e. connection where the objects themselves do
;; not overlap with one another).
(subclass-of externally-connected connected)
(documentation externally-connected "Means that the arguments of the relation are "connected", but that they do not "overlap")
(=>
(externally-connected ?X ?Y)
(not
(overlaps ?X ?Y)))
;; Definition of the class 'SelfConnectedObject' (from Casati and Varzi): ?x is a SelfConnected
;; just in case ?x does not consist of two or more disconnected parts.
(subclass-of SelfConnectedObject CorpuscularObject)
(documentation SelfConnectedObject "Something is a SelfConnectedObject just in case it does not consist of two or more disconnected parts.")
(<=>
(instance-of ?X SelfConnectedObject)
(forall (?Y ?Z)
(=>
(equal ?X (MereologicalSumFn ?Y ?Z))
(connected ?Y ?Z)))
;; Definition of the class 'ClosedObject'
(subclass-of ClosedObject CorpuscularObject)
(<=>
(instance-of ?X ClosedObject)
(equal ?X (ClosureFn ?X)))
;; Definition of 'BoundaryClass' (the class of boundaries)
(subclass-of BoundaryClass CorpuscularObject)
(documentation BoundaryClass "This is just a convenient way of aggregating all of the boundaries of objects.")
(<=>
(instance-of ?X BoundaryClass)
(exists (?Y)
(boundary ?X ?Y)))
;;;;;;;;;;;;;;;;;;;;;
;; POSITIONS ;;
;;;;;;;;;;;;;;;;;;;;;
;; This section aligns the content in the Positions ontology of the ITBM-CRN group. This content
;; is a set of predicates for describing spatial relations. At this point (01/12/01), very
;; few axioms are given. Eventually, the meaning of all of these predicates should be cashed
;; out with the relations defined in the earlier section "Mereotopological Definitions/Axioms".
(instance-of position BinaryRelation)
(nth-domain position 1 Object)
(nth-domain position 2 Object)
(documentation position "(position ?X ?Y) means that ?X is positioned with respect to ?Y in some way. This is a very general predicate whose main utility is to function as an umbrella for the more specific positional predicates.")
(subclass-of above position)
(documentation above "This is a cognitive primitive, derived from the up/down schema and not involving contact. A possible formalization of the medical meaning must take into account the conventional body directions; though, there is no unique direction hierarchy guiding the application of this relation to anatomical spaces.")
(=>
(above ?X ?Y)
(not
(connected ?X ?Y)))
(subclass-of adjacent position)
(documentation adjacent "Close to, near or abutting another physical unit with no other
structure of the same kind intervening. This includes adjoins, abuts, is contiguous to, is
juxtaposed, and is close to.")
(=>
(adjacent ?X ?Y)
(or
(near ?X ?Y)
(connected ?X ?Y)))
(subclass-of along position)
(documentation along "(along ?X ?Y) means that an object ?X shares the region of ?Y at least as far the extension of one dimension is concerned.")
(subclass-of behind position)
(documentation behind "This is a cognitive primitive, derived from the front/back schema; a possible formalization of the medical meaning must take into account the conventional body directions; though, there is no unique direction hierarchy guiding the application of this relation to anatomical spaces.")
(subclass-of below position)
(<=>
(below ?X ?Y)
(above ?Y ?X))
(instance-of between TernaryRelation)
(nth-domain between 1 Object)
(nth-domain between 2 Object)
(nth-domain between 3 Object)
(=>
(between ?X ?Y ?Z)
(and
(left-of ?Y ?X)
(left-of ?X ?Z)))
(subclass-of contains position)
(documentation contains "The surrounding relation for masses.")
(=>
(contains ?X ?Y)
(forall (?Z)
(=>
(part-of ?Z ?Y)
(exists ?U
(interior-part-of ?U ?X)
(located-at ?Z ?U)))))
(subclass-of crosses-over position)
(documentation crosses-over "(crosses-over ?X ?Y) means that X crosses-through the region of
y, without overlapping y.")
(=>
(crosses-over ?X ?Y)
(not
(connected ?X ?Y)))
(subclass-of crosses-through position)
(documentation crosses-through "Here: x crosses-through y equals to x overlaps y along at least one whole dimension (length, width or depth), say the interiors of x and y overlap.")
(subclass-of left-of position)
(documentation left-of "This is a cognitive primitive, derived from the left/right schema; a possible formalization of the medical meaning must take into account the conventional body directions; though, there is no unique direction hierarchy guiding the application of this relation to anatomical spaces.")
(subclass-of near position)
(documentation near "Specialized common sense adjacency without contact;
based on implicit scale and distance less than the diameter of the smaller object;
alternatively, based on the smallest distance among the higher granularity objects.
Eg, in cell C near object P, P is the less distant object of a higher granularity
than C.")
(=>
(near ?A ?B)
(or (exists (?C ?D ?E)
(and (the-smaller ?A ?B ?E)
(diameter ?E ?D)
(distance ?A ?B ?C)
(lessThan ?C ?D)))
(not (exists (?Z)
(or (and (exists (?F)
(and (the-finer-granularity ?A ?Z ?F)
(equal ?F ?A)))
(same-granularity ?B ?Z)
(exists (?G ?H)
(and (distance ?B ?A ?H)
(distance ?Z ?A ?G)
(lessThan ?G ?H)))
(different ?B ?Z))
(and (exists (?I)
(and (the-finer-granularity ?B ?Z ?I)
(equal ?I ?B)))
(same-granularity ?A ?Z)
(exists (?J ?K)
(aND (distance ?A ?B ?K)
(distance ?Z ?B ?J)
(lessThan ?J ?K)))
(different ?A ?Z)))))))
(subclass-of on position)
(documentation on "This is a cognitive primitive, derived from the up/down schema and involving contact. A possible formalization of the medical meaning must take into account the conventional body directions; though, there is no unique direction hierarchy guiding the application of this relation to anatomical spaces.")
(=>
(on ?X ?Y)
(connected ?X ?Y))
(subclass-of right-of position)
(<=>
(right-of ?X ?Y)
(left-of ?Y ?X))
(subclass-of surrounds position)
(documentation surrounds "limits, bounds, confines, encloses or circumscribes, but excluding the containment of substances. Here it is defined by stating that x surrounds y iff the interior of x wholly contains y.")
(subclass-of traverses position)
(documentation traverses "Crosses or extends across another physical structure or
area. This includes crosses over and crosses through.")
(subclass-of under position)
(=>
(under ?X ?Y)
(or
(on ?Y ?X)
(above ?Y ?X)))
;;;;;;;;;;;
;; NOTES ;;
;;;;;;;;;;;
;; We need to be able to distinguish instances of Continuant which are stuffs
;; (e.g. water, oxygen, sand) from instances of Continuant which are objects
;; (e.g. table, jacket, notebook). From what I can see, there is no provision
;; for this distinction in Sowa's ontology. Perhaps we could divide 'Continuant'
;; into two disjoint classes, viz. Continuant-Stuff and Continuant-Object.
;; The following is a possible means of axiomatizing the distinction between 'ContinuousObject'
;; and 'CorpuscularObject' in the upper level ontology. This is borrowed from the Morphology
;; ontology developed by ITBM-CNR (in particular it is taken from the definitions of Heteromerous
;; and Homeomerous in this ontology). The axioms are commented out for the time being, because
;; they are framed in terms of 'StuffType' which has not yet been included in the ontology.
;; (=>
;; (instance-of ?X CorpuscularObject)
;; (exists (?Y ?Z)
;; (and
;; (instance-of ?Y StuffType)
;; (instance-of ?Z StuffType)
;; (constituent-material-of ?Y ?X)
;; (constituent-material-of ?Z ?X)
;; (not (subclass-of ?Y ?Z))
;; (not (subclass-of ?Z ?Y)))))
;; (=>
;; (instance-of ?X ContinuousObject)
;; (exists (?Y)
;; (and
;; (instance-of ?Y StuffType)
;; (constituent-material-of ?Y ?X)
;; (forall (?Z)
;; (=>
;; (and
;; (instance-of ?Z StuffType)
;; (constituent-material-of ?Z ?X)
;; (equal ?Z ?Y))))))
;; We may want to include something like the following axioms at some point.
;;(=>
;; (playsRole ?Act ?Ent ?Role)
;; (capableOfDoing ?Ent ?Act ?Role))
;;(=>
;; (and
;; (playsRole ?Act ?Res Resource)
;; (ends ?Act ?Time)
;; (holdsIn (STIB ?Time) (amountAvailable ?Res ?Amt1))
;; (holdsIn (STIF ?Time) (amountAvailable ?Res ?Amt2)))
;; (greaterThan ?Amt1 ?Amt2))
;; Formulate an axiom to the effect that a DiscreteProcess consists of interleaved
;; events and states
;; The following is a provisional addition to the top level of the ontology. The purpose
;; of this addition is to accommodate normative notions. If this addition is embraced by
;; the other SUO participants and if it is deemed acceptable in other respects it will be ;; commented out.
;; (subclass-of Normative Entity)
;; (subclass-of NormativeProposition Normative)
;; (subclass-of NormativeProposition Proposition)
;; (subclass-of Obligation NormativeProposition)
;; (subclass-of Agreement NormativeProposition)
;; (subclass-of JudgementOfEtiquette NormativeProposition)
;; (subclass-of AestheticJudgement NormativeProposition)
;; (subclass-of InstitutionalObligation Obligation)
;; (subclass-of PersonalObligation Obligation)
;; (subclass-of ReligiousObligation InstitutionalObligation)
;; (subclass-of LegalObligation InstitutionalObligation)
;; The following is another provisional addition to the top level of the ontology. This
;; addition locates the crucial notions of 'WavePropagation', 'ElectronicWave', and
;; 'ElectronicSignal' within the existing framework of concepts.
;; (subclass-of WavePropagation KineticForm)
;; (subclass-of ElectronicWave WavePropagation)
;; (subclass-of ElectronicSignal ElectronicWave)
;; (subclass-of ElectronicSignal Sign)
;; The following is the original hierarchy of constants under 'Role' in Sowa's ontology. Since
;; this part of the ontology has been superceded, it has been commented out.
;;(subclass-of PrehendingEntity Role)
;;(subclass-of PrehendedEntity Role)
;;(subclass-of Composite PrehendingEntity)
;;(subclass-of Correlative PrehendingEntity)
;;(subclass-of Correlative PrehendedEntity)
;;(subclass-of Component PrehendedEntity)
;;(subclass-of Whole Composite)
;;(subclass-of Substrate Composite)
;;(subclass-of Part Component)
;;(subclass-of Property Component)
;;(subclass-of Piece Part)
;;(subclass-of Participant Part)
;;(subclass-of Stage Part)
;;(subclass-of Attribute Property)
;;(subclass-of Manner Property)
;;(subclass-of Determinant Participant)
;;(subclass-of Source Participant)
;;(subclass-of Product Participant)
;;(subclass-of Immanent Participant)
;;(subclass-of Initiator Determinant)
;;(subclass-of Initiator Source)
;;(subclass-of Resource Source)
;;(subclass-of Resource Immanent)
;;(subclass-of Goal Determinant)
;;(subclass-of Goal Product)
;;(subclass-of Essence Product)
;;(subclass-of Essence Immanent)
;;(subclass-of Agent Initiator)
;;(subclass-of Recipient Goal)
;;(subclass-of Beneficiary Recipient)
;;(subclass-of Completion Goal)
;;(subclass-of Destination Goal)
;;(subclass-of Duration Resource)
;;(subclass-of Effector Initiator)
;;(subclass-of Experiencer Goal)
;;(subclass-of Instrument Resource)
;;(subclass-of Location Essence)
;;(subclass-of Matter Resource)
;;(subclass-of Medium Resource)
;;(subclass-of Origin Initiator)
;;(subclass-of Path Resource)
;;(subclass-of Patient Essence)
;;(subclass-of PointInTime Essence)
;;(subclass-of Result Goal)
;;(subclass-of Start Initiator)
;;(subclass-of Theme Essence)
;; We probably will need to add back some notion of 'Intention' or 'IntentionalEntity' at
;; some point.
;;
;; (documentation IntentionalEntity "Examples of intentions include the hopes, fears, wishes,
;; and purposes that mediate some agent's actions.")