SUO: Re: TLC in KIF
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Adam, Chris, Ian, & KIF'n Cousins All,
I had been reserving my comments on this translation
of John Sowa's "Top Level Categories" (TLC) into KIF
until such time as the author himself could have his
say on the result. As that earnestly to be desired
outcome does not appear to be forthcoming any time
soon, or in any sort of direct way, and it has just
now occurred to me -- duh! -- that perhaps this has
already happened in one of those apparently all the
more frequent off-list discussion and decision-making
bodies with which this ostensibly "open" forum has now
saddled itself, I guess that I might as well go ahead
and toss my tuppence worth into the pot, as it were.
I would like to try and make at least one thing clear right here
at the beginning, so that nobody takes any of this too personally
or too pointedly, namely, that most of what I have to say is not
specific to KIF, not by any means, but would apply equally well
to that whole tradition of formalities in logic that have come
to be foist-order-lodged in our intellects by the lights and
by the likes of Frege, Russell, and Wittgenstein.
I also think that it might contribute to our mutual understanding
if I explain one or two aspects of my own background. I was not
always this skeptical about the potential of FOL as we know it --
I came by my aporetics quite honestly, in the way that I have had
to learn all of my lessons, the hard way, through disappointment
in following through with my former beliefs. I was once in fact
what you might call a "True Believer" in the point of view that
used to be known as "logicism", namely, the idea that every form
of mathematical reasoning reduces to a matter of deductive logic.
This is the POV that I took into my graduate studies in maths,
and this is the POV that I revived yet another time when I set
about trying to develop qualitative methods in psychology, and
this is the angle at which I just had to keep on butting my head,
one more time for good measure, when I tried to integrate my early
efforts into a try at AI. Now, a person takes an obvious risk in
airing out his own failed trials in this way -- it is so easy for
anybody to say "Well, that's just him" and go back to trying the
same old, same old things for all that anybody's worth, one more
time, with a few innovations, always a few more novelties to try.
But I will go ahead, anyway, and state the lesson that I, for one,
learned from my honest, if naive, attempts, and that is just that
formalisms like the "logic of deductive inference" (LODI) and the
"theory of classes and sets" (TOCAS) are perfectly -- well, almost
perfectly -- good forms of representation for succintly summarizing
what you have discovered, at any rate, once you have discovered it
usually by any other means possible, in what is often called the
"context of justification and review" (COJAR), but that these
brands of formalism are darn near useless and a positivistic
nuisance when it comes to the discovery phases of the overall
"context of inquiry" (COI) itself.
Well, all of my pre-ambling took longer than I thought it would,
and so I will have to break now and try to get back to the main
part of your translation piece later.
Cheers,
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Original Message:
Adam Pease wrote
> SUO: Sowa's Top Level
>
> ---------------------------------------------------------------------------
>
> * To: standard-upper-ontology@ieee.org
> * Subject: SUO: Sowa's Top Level
> * From: Adam Pease <apease@teknowledge.com>
> * Date: Wed, 22 Nov 2000 08:10:37 -0800
> * Reply-To: Adam Pease <apease@teknowledge.com>
> * Sender: owner-standard-upper-ontology@ieee.org
>
> ---------------------------------------------------------------------------
>
> Folks,
> Here is an SUO-KIF version of John Sowa's upper level ontology
> thanks to Chris Menzel and Ian Niles. All comments are welcome.
>
> Adam
>
> ;; A KIF encoding of John Sowa's upper ontology found at
> ;; http://www.bestweb.net/~sowa/ontology/toplevel.htm and in
> ;; Chapter 2 of his book _Knowledge Representation_, Brooks/Cole, 2000.
>
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
> ;; P R E F A C E ;;
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
>
> ;; METALINGUISTIC DEFINITIONS
> ;;
> ;; Metalinguistic definitions provide us with theoretical
> ;; justifications for the use 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))))
> ;;
>
> ;; THE LANGUAGE OF SOWA'S UPPER LEVEL ONTOLOGY
> ;;
> ;; 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"). Primitive
> ;; constants, primitive predicates, and defined predicates are
> ;; listed below. Note that 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).
> ;;
> ;;;;;;;;;;;;;;;;;;;;;;;;;
> ;; Primitive constants ;;
> ;;;;;;;;;;;;;;;;;;;;;;;;;
> ;;
> ;; Entity, Absurdity, Independent, Relative, Mediating, Physical,
> ;; Abstract, Continuant, Occurrent, Actuality, Form, Prehension,
> ;; Proposition, Nexus, Intention, Object, Process, Schema, Script,
> ;; Juncture, Participation, Description, History, Structure,
> ;; Situation, Reason, Purpose
> ;;
> ;;;;;;;;;;;;;;;;;;;;;;;;;;
> ;; Primitive predicates ;;
> ;;;;;;;;;;;;;;;;;;;;;;;;;;
> ;;
> ;; 1-place: Entity, Class
> ;;
> ;; 2-place: has, instance-of, subclass-of, temp-part-of, spatial-part-of
> ;;
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
> ;; Primitive (non-KIF) operators ;;
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
> ;;
> ;; nec, poss
> ;;
> ;;;;;;;;;;;;;;;;;;;;;;;;
> ;; Defined predicates ;;
> ;;;;;;;;;;;;;;;;;;;;;;;;
> ;;
> ;; 2-place: disjoint
> ;;
> ;;;;;;;;;;;;;;;;;;;;;;;;;
> ;; Borrowed predicates ;;
> ;;;;;;;;;;;;;;;;;;;;;;;;;
> ;;
> ;; From an ontology of space and time
> ;;
> ;; 1-place: timepoint
> ;;
> ;; 2-place: before, beforeEq, exists-at, located-at
>
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
> ;; O N T O L O G Y ;;
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
>
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;; DEFINITIONS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
>
> (documentation disjoint "Classes X and Y are disjoint iff they share no instances.")
>
> (forall (?class1 ?class2)
> (<=> (disjoint ?class1 ?class2)
> (and (Class ?class1)
> (Class ?class2)
> (not (exists (?x)
> (and (instance-of ?x ?class1)
> (instance-of ?x ?class2)))))))
>
> ;;;;;;;;;;;;;;; AXIOMS EXPRESSING THE CLASS HIERARCHY ;;;;;;;;;;;;;;;;;
>
> (subclass-of Independent Entity)
> (subclass-of Relative Entity)
> (subclass-of Mediating Entity)
> (subclass-of Physical Entity)
> (subclass-of Abstract Entity)
> (subclass-of Continuant Entity)
> (subclass-of Occurrent Entity)
>
> (subclass-of Actuality Independent)
> (subclass-of Actuality Physical)
> (subclass-of Form Independent)
> (subclass-of Form Abstract)
> (subclass-of Prehension Physical)
> (subclass-of Prehension Relative)
> (subclass-of Proposition Relative)
> (subclass-of Proposition Abstract)
> (subclass-of Nexus Physical)
> (subclass-of Nexus Mediating)
> (subclass-of Intention Abstract)
> (subclass-of Intention Mediating)
>
> (subclass-of Object Actuality)
> (subclass-of Object Continuant)
> (subclass-of Process Actuality)
> (subclass-of Process Occurrent)
> (subclass-of Schema Form)
> (subclass-of Schema Continuant)
> (subclass-of Script Form)
> (subclass-of Script Occurrent)
> (subclass-of Juncture Prehension)
> (subclass-of Juncture Continuant)
> (subclass-of Participation Prehension)
> (subclass-of Participation Occurrent)
> (subclass-of Description Proposition)
> (subclass-of Description Continuant)
> (subclass-of History Proposition)
> (subclass-of History Occurrent)
> (subclass-of Structure Nexus)
> (subclass-of Structure Continuant)
> (subclass-of Situation Nexus)
> (subclass-of Situation Occurrent)
> (subclass-of Reason Intention)
> (subclass-of Reason Continuant)
> (subclass-of Purpose Intention)
> (subclass-of Purpose Occurrent)
>
> ;;;;;;;;;;;;;;;;;; DOCUMENTATION FOR THESE CLASSES ;;;;;;;;;;;;;;;;;;;;
>
> (documentation Entity "The universal class of individuals, which has no differentiae.")
>
> (documentation Absurdity "The absurd class, which inherits all differentiae.")
>
> (documentation Abstract "Pure information as distinguished from any particular encoding
> of the information in a physical medium.")
>
> (documentation Physical "An entity that has a location in space-time.")
>
> (documentation Actuality "A physical entity (P) whose existence is
> independent (I) of any other entity. As instances, the category
> Actuality includes both objects and processes. The term is taken
> from Whitehead, who used it as a synonym for actual entity, which
> he considered the equivalent of Aristotle's ousia and Descartes's
> res vera.")
>
> (documentation Continuant "A continuant is an entity whose identity
> continues to be recognizable over some extended interval of time.")
>
> (documentation Description "A proposition (RA) about a continuant (C).
> A description is a proposition that states how some schema characterizes
> some aspect or configuration of a continuant.")
>
> (documentation Form "Abstract information (A) independent (I) of any encoding
> or embodiment. Forms can be said to exist in the same sense as mathematical
> objects such as sets and relations, but instances of forms cannot exist at
> a particular place and time without some physical encoding or embodiment.
> Whitehead called them "eternal objects" because they are independent of
> space and time.")
>
> (documentation History "A proposition (RA) about an occurrent (O).
> A history is a proposition (RA) that relates some script (IAO) to
> the stages of some occurrent (O). A computer program, for example,
> is a script (IAO); a computer executing the program is a process (IPO);
> and the abstract information (A) encoded in a trace of the instructions
> executed is a history (RAO). Like any proposition, a history need not be true,
> and it need not be predicated of the past: a myth is a history of an imaginary past;
> a prediction is a history of an expected future; and a scenario is a history of some
> hypothetical occurrent.")
>
> (documentation Independent "An entity characterized by some inherent
> Firstness, independent of any relationships it may have to other entities.
> Formally, Independent is a primitive for which the has-test (cf. Section 2.4
> of _Knowledge Representation_) need not apply. If x is an independent entity,
> it is not necessary that there exists an entity y such that x has y or y has x.")
>
> (documentation Intention "Abstraction (A) considered as mediating (M) other entities.
> Examples of intentions include the hopes, fears, wishes, and purposes that mediate
> some agent's actions.")
>
> (documentation Juncture "A prehension (RP) considered as a continuant (C)
> during some time interval. The prehending entity is an object (IPC) in
> a stable relationship to some prehended entity during that interval.
> An example of a juncture is the relationship between two adjacent
> stones in an arch. The arch itself is a nexus that both mediates
> and consists of the multiple junctures.")
>
> (documentation Mediating "An entity characterized by some Thirdness
> that brings other entities into a relationship. An independent entity
> need not have any relationship to anything else, a relative entity must
> have some relationship to something else, and a mediating entity creates
> a relationship between two other entities. An example of a mediating entity
> is a marriage, which creates a relationship between a husband and a wife.
> According to Peirce, the defining aspect of Thirdness is 'the conception
> of mediation, whereby a first and a second are brought into relation.")
>
> (documentation Nexus "A physical entity (P) mediating (M) two or
> more other entities. Each nexus is a bundle of prehensions, which
> may be the junctures of an object or the participants of a process.
> Examples include an arch that consists of junctures of stones or
> an action that consists of what one participant called an agent
> is doing to another participant called a patient.")
>
> (documentation Object "Actuality (IP) considered as a continuant (C),
> which retains its identity over some interval of time. Although no
> physical entity is ever permanent, an object can be recognized by
> identity conditions that remain stable during its lifetime.
> 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 is a primitive that
> satisfies the following axioms: \
> * The temporal parts of an occurrent, which are called stages,
> exist at different times. \
> * The spatial parts of an occurrent, which are called participants,
> may exist at the same time, but an occurrent may have different
> participants at different stages.\
> * There are no identity conditions that can be used to identify
> two occurrents that are observed in nonoverlapping space-time regions. \
>
> (NOTE: The notions identity conditions and observation are not axiomatized
> in this ontology, so this is not an actual axiom of the ontology, unlike the
> two axioms above. (Though those two required adding some notions that are only
> implicit in Sowa's ontology, e.g., the relations "exists-at" and "located-at".)
> 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 Participation "A prehension (RP) considered as an occurrent (O)
> during the interval of interest. The prehending entity is a process (IPO),
> and the prehended entity is called a participant.")
>
> (documentation Process "Actuality (IP) considered as an occurrent (O)
> 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 Prehension "A physical entity (P) relative (R)
> to some entity or entities. The has-test is used to check
> whether an entity x prehends an entity y. If so, the
> prehension may be expressed has(x,y).")
>
> (documentation Proposition "An abstraction (A) that relates (R)
> some entity or entities. 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 the form labeled Cat characterizes the entity
> named Yojo. According to Peirce and Whitehead, more complex propositions
> are asserted by constructing a compound predicate, such as a mathematical
> expression or a diagram, and using it to characterize the prehensions
> that relate multiple entities.")
>
> (documentation Purpose "Intention (MA) that has the form of an occurrent (O).
> As an example, the words and notes of the song "Happy Birthday" constitute
> a script (IAO); a description of how people at a party sang the song is
> history (RAO); and the intention (MA) that explains the situation (MPO)
> is a purpose (MAO). The basic axioms for Purpose are inherited from its
> supertypes Mediating, Abstract, and Occurrent. Some lower level axioms
> relate purposes to actions and agents:
> (1) Time sequence. If an agent x performs an act y whose purpose
> is a situation z, the start of y occurs before the start of z.
> (2) Contingency. If an agent x performs an act y whose purpose is
> a situation z described by a proposition p, then it is possible
> that z might not occur or that p might not be true of z.
> (3) Success or failure. If an agent x performs an act y whose purpose
> is a situation z described by a proposition p, then x is said to be
> successful if z occurs and p is true of z. otherwise, x is said to
> have failed. Note that to express these axioms we would need to
> introduce lower level classes like "agent" and 'action'.")
>
> (documentation Reason "Intention (MA) that has the form of a continuant (C).
> Unlike a simple description (Secondness), a reason explains an entity in terms
> of an intention (Thirdness). For a birthday party, a description might list the
> presents, but a reason would explain why the presents are relevant to the party.")
>
> (documentation Relative "An entity in a relationship to some other entity.
> (See the ISSUE above accompanying the formal axiom for Relative.")
>
> (documentation Schema "A form (IA) that has the structure of a continuant (C).
> A schema is an abstract form (IA) whose structure 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 "A form (IA) that has the structure of an occurrent (O).
> A script is an abstract form (IA) that 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 Situation "A nexus (MP) considered as an occurrent (O).
> A situation mediates the participants of some process, whose stages
> may involve different participants at different times.")
>
> (documentation Structure "A nexus (MP) considered as a continuant (C).
> A structure mediates multiple objects whose junctures constitute the structure.")
>
> ;;;;;;;;;;;;;;;;;;;;;;;;;;; GENERAL AXIOMS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;
>
> (documentation "AXIOM: 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))))))
>
> ;; ISSUE: Given that we are using a modal language, the subclass-of
> ;; relation is arguably definable: X is a subclass of Y if and only if
> ;; X and Y are classes and, necessarily, every instance of X is an
> ;; instance of Y.
>
> (documentation "AXIOM: Every class is a subclass of itself.")
>
> (forall (?class)
> (=> (Class ?class)
> (subclass-of ?class ?class)))
>
> ;; Axioms for the *predicate* "Entity". It turns out to be convenient
> ;; to introduce "Entity" as both a predicate true of all entities and
> ;; as a constant denoting the class of entities.
>
> (documentation "AXIOM: There are entities.")
>
> (exists (?x) (Entity ?x))
>
> (documentation "AXIOM: Everything is either a class or an entity, but not both.")
>
> (forall (?x)
> (and (or (Class ?x)
> (Entity ?x))
> (<=> (Entity ?x)
> (not (Class ?x)))))
>
> (documentation "AXIOM: Only entities are instances of classes, and only classes have instances.")
>
> (forall (?x)
> (=> (instance-of (?instance ?class))
> (and (Entity ?instance)
> (Class ?class))))
>
> ;; Axioms for the *constant* "Entity". Syntactically, we can treat
> ;; the predicate `Entity' and the constant `Entity' as distinct things
> ;; that look the same; alternatively, we can simply allow `Entity' to
> ;; be both a predicate and a constant. Semantically, the interpretations
> ;; of the predicate "Entity" and the constant "Entity" may or may not turn out
> ;; to be the same thing.
>
> (documentation "AXIOM: Entity (the class) consists of exactly
> the entities (the things to which the `Entity' predicate applies )")
>
> (forall (?x)
> (<=> (Entity ?x)
> (instance-of ?x Entity)))
>
> ;; THEOREM: Entity is a class.
>
> (Class Entity)
>
> ;; PROOF: By the two preceding axioms, there is at least one entity
> ;; ?x, and hence ?x is an instance-of Entity. Hence, by the axiom
> ;; above for instance-of, Entity must be a class (since only classes
> ;; have instances).
>
> (documentation "AXIOM: Every class is a subclass of Entity.")
>
> (forall (?c)
> (=> (Class ?c)
> (subclass-of ?c Entity)))
>
> (documentation "AXIOM: The has relation holds between entities.")
>
> (nth-domain has 1 Entity 2 Entity)
>
> (documentation "AXIOM: Absurdity is a class.")
>
> (Class Absurdity)
>
> (documentation "AXIOM: Absurdity has no instances.")
>
> (not (exists (?x) (instance-of ?x Absurdity)))
>
> (documentation "AXIOM: Absurdity is a subclass of every class.")
>
> (forall (?c)
> (=> (Class ?c)
> (subclass-of Absurdity ?c)))
>
> (documentation "AXIOM: Abstract is a class.")
>
> (Class Abstract)
>
> (documentation "AXIOM: ?x is abstract iff it has neither a spatial nor temporal location.")
>
> ;; NOTE: "located-at" and "exists-at" are spatial and temporal
> ;; predicates, respectively, that are not axiomatized here.
> ;; "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.
>
> (forall (?x)
> (<=> (instance-of ?x Abstract)
> (and (not (exists (?y)
> (or (located-at ?x ?y)
> (exists-at ?x ?y)))))))
>
> (documentation "AXIOM: ?x is physical if and only if it exists at some location at some time.")
>
> (forall (?x)
> (<=> (Physical ?x)
> (exists (?y ?z)
> (and (located-at ?x ?y)
> (exists-at ?x ?z)))))
>
> (documentation "THEOREM: Abstract and Physical are disjoint.")
>
> (disjoint Abstract Physical)
>
> ;; Proof: Immediate from the axioms for Abstract and Physical.
>
> (documentation "AXIOM: An independent entity need not bear the "has" relation to anything.")
>
> (forall (?x)
> (=> (Independent ?x)
> (not (nec (exists (?y)
> (or (Has ?x ?y)
> (Has ?y ?x)))))))
>
> (documentation "AXIOM: 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. This axiom is only implicit in Sowa's ontology.
> Again, it appeals to an auxiliary ontology of timepoints.")
>
> (forall (?x)
> (=> (instance-of ?x Continuant)
> (exists (?t1 ?t2)
> (and (timepoint ?t1)
> (timepoint ?t2)
> (before ?t1 ?t2)
> (forall (?t)
> (=> (and (beforeEq ?t1 t)
> (beforeEq (t ?t2)))
> (exists-at ?x ?t)))))))
>
> (documentation "AXIOM: If a mediating entity ?m has ?x and ?y,
> then either ?x has ?y or vice versa.")
>
> (forall (?x ?y ?z)
> (=> (and (instance-of ?m Mediating)
> (has ?m ?x)
> (has ?m ?y))
> (nec (or (has ?x ?y) (has ?y ?x)))))
>
> (documentation "AXIOM: Continuant and Occurrent are disjoint.")
>
> (disjoint Continuant Occurrent)
>
> (documentation "AXIOM: The temp-part-of relation holds between entities and occurrents")
>
> (nth-domain temp-part-of 1 Entity 2 Occurrent)
>
> (documentation "AXIOM: 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 exist across intervals of time?
>
> (forall (?occ ?x)
> (=> (and (instance-of ?occ Occurrent)
> (temp-part-of ?x ?occ))
> (exists (?t)
> (exists-at ?x ?t))))
>
> (documentation "AXIOM: The spatial-part-of relation holds between entities and occurrents")
>
> (nth-domain spatial-part-of 1 Entity 2 Occurrent)
>
> (documentation "AXIOM: Each spatial part of an occurrent exists at some location.")
>
> (forall (?occ ?x)
> (=> (and (instance-of ?occ Occurrent)
> (spatial-part-of ?x ?occ))
> (exists (?loc)
> (located-at ?x ?loc))))
>
> (documentation "AXIOM: Occurrents have temporal parts")
>
> (forall (?occ)
> (=> (instance-of ?occ Occurrent)
> (exists (?x)
> (temp-part-of ?x ?occ))))
>
> (documentation "AXIOM: Occurrents have spatial parts")
>
> (forall (?occ)
> (=> (instance-of ?occ Occurrent)
> (exists (?x)
> (spatial-part-of ?x ?occ))))
>
> (documentation "AXIOM: Every relative entity necessarily bears the
> has relation to some entity, or some entity hears that relation to it.")
>
> ;; ISSUE: If "has" is not characterized carefully this axiom could
> ;; turn out to be trivial. For example, most independent physical
> ;; objects necessarily have parts. But I believe physical objects
> ;; per se are paradigms of independent (hence non-relative) objects
> ;; for Sowa. So the question is how to avoid the consequence that
> ;; intuitively independent entities turn out to be relative.
> ;; Qualification of the "has" relation seems to be the best way out here.
> ;; For instance, one could introduce a part-of relation and then explicitly
> ;; deny that if x is a part of y, then y has x. But this approach is dubious --
> ;; how does one distinguish legitimate cases of having -- e.g., a marriage has
> ;; a husband, a husband a wife -- from illegitimate?
>
> (forall (?x)
> (=> (instance-of ?x Relative)
> (nec (exists (?y)
> (or (has ?x ?y)
> (has ?y ?x))))))
>
> (documentation "AXIOM: Independent and Relative are disjoint.")
>
> (disjoint Independent Relative)
>
> (documentation "AXIOM: Relative and Mediating are disjoint.")
>
> (disjoint Relative Mediating)
>
> (documentation "AXIOM: Independent and Relative are disjoint.")
>
> (disjoint Independent Relative)
>
> ;;;;;;;;;;;;;;;;;;;;;;; SUPPLEMENTARY ONTOLOGY ;;;;;;;;;;;;;;;;;;;;;;;;
>
> ;; A minimal ontology of timepoints is included below
> ;; (from the NIST Process Specfication Language (PSL) project:
> ;; http://www.nist.gov/psl). An analogous ontology for spatial
> ;; locations is needed as well. Sowa has expressed (controversial)
> ;; reservations about the assumption that the before relation is
> ;; a total ordering; if necessary, the axiom can always be dropped.
> ;; Also, sufficient background for the "exists-at" predicate is also
> ;; needed -- but this will require some decisions about where events fit
> ;; into Sowa's picture, as well as how to ascribe temporal properties
> ;; (like the beginning of a thing's existence) to objects.
>
> (documentation beforeEq "Timepoint ?t1 is beforeEq timepoint ?t2
> iff ?t1 is before or equal to ?t1.")
>
> (forall (?t1 ?t2)
> (<=> (beforeEq (?t1 ?t2)
> (and (timepoint ?t1) (timepoint ?t2)
> (or (before ?t1 ?t2) (= ?t1 ?t2))))))
>
> (documentation "AXIOM: The exists-at relation holds between physical things and timepoints.")
>
> (nth-domain exists-at 1 Physical 2 timepoint)
>
> (documentation "AXIOM: The before relation only holds between timepoints.")
>
> (nth-domain before 1 timepoint 2 timepoint)
>
> (documentation "AXIOM: The before relation is a total ordering.")
>
> (forall (?t1 ?t2: (and (timepoint ?t1) (timepoint ?t2)))
> (or (= ?t1 ?t2)
> (before ?t1 ?t2)
> (before ?t2 ?t1)))
>
> (documentation "AXIOM: The before relation is irreflexive.")
>
> (forall (?t1)
> (not (before ?t1 ?t1)))
>
> (documentation "AXIOM: The before relation is transitive.")
>
> (forall (?t1 ?t2 ?t3)
> (=> (and (before ?t1 ?t2) (before ?t2 ?t3))
> (before ?t1 ?t3)))
>
> -----------------
> Adam Pease
> Teknowledge
> (650) 424-0500 x571
>
> ---------------------------------------------------------------------------
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤