idef3_kbsi_report (1013870), страница 42
Текст из файла (страница 42)
For amore robust version, the explicit set theoretic apparatus included in KIF could be added at thispoint, but this is unnecessary for purposes here; see (Genesereth & Fikes, 1992) for details of theset theory included in KIF.A.5.2Basic Situation Theoretic Semantic CategoriesIn this section the basic semantic categories of situation theory are introduced andcharacterized.(define-relation infon (?x))(define-relation situation (?x))(define-relation UOB (?x))(define-relation COE (?x))(define-relation process (?x))(define-relation interval (?x))(define-relation polarity)A single axiom expresses that the basic semantic categories are all disjoint; e.g., noindividual is an infon, function, or relation.(forall (?x ?y)(=> (and (or (= ?x individual) (= ?x infon) (= ?x relation) (= ?x situation)(= ?x UOB) (= ?x COE) (= ?x process) (= ?x polarity))(or (= ?y individual) (= ?y infon) (= ?y relation) (= ?y situation)(= ?y UOB) (= ?y COE) (= ?y process) (= ?y polarity))(=/ ?x ?y))(forall ?z (not (and (?x ?z) (?y ?z))))))210A.5.2.1First-order RelationsIn the version of situation theory developed here, infons are constructed only out of firstorder relations and individuals.
Hence, the notion of a first-order relation needs to be definedexplicitly and axiomatized with an appropriate schema.(define-relation FO-relation (?rel):=> (relation ?rel))A first-order relation is a relation that can only be true of n-tuples of individuals.(forall (?rel : (FO-relation ?rel) (= (arity ?rel) n)))(forall (var1 . . . varn : (?rel var1 . . . varn))(and (individual var1) . .
. (individual varn))))Recall that change in the extension of a typical first-order relation over time is captured byincluding a parameter for temporal intervals among its arguments. For example, the relationwalks is taken to be a 2-place relation that holds between an individual b and an interval t just incase b walks throughout the interval t. Because intervals are themselves individuals, this isaccommodated by the above definition.A.5.2.2Axioms for Infon TermsGiven the notion of a first-order relation, axioms can be given that express what is requiredfor an infon term to denote a legitimate infon (as opposed to the null object).A basic infon term denotes an infon if and only if it consists of a term denoting an n-placefirst-order relation followed by n terms denoting individuals and a term denoting a polarity.(forall (?rel var1 .
. . varn ?pol)(<=> (infon (?r var1 . . . varn ?pol))(and (FO-relation ?r)(individual var1)...(individual varn)(polarity ?p))))A conjunctive (disjunctive) infon term denotes an infon if and only if each conjunt (disjunct)denotes an infon.(forall (?inf1 ?inf2)(<=> (and (infon (and ?inf1 ?inf2)))(and (infon ?inf1) (infon ?inf2))))(forall (?inf1 ?inf2)(<=> (and (infon (or ?inf1 ?inf2)))211(and (infon ?inf1) (infon ?inf2))))Analogous axioms for quantified infons must be stated as a schema. Let Q be any quantifier,var any variable, and infterm be any infon term. If var occurs free as the first term in any atomicinfon in infterm, then(<=> (infon (Q var infterm))(Q (var : (FO-relation var)) (infon infterm)))).Similarly, if var does not occur free as the first term in any atomic infon term in infterm (i.e.,occurs bound, or occurs free elsewhere than as the first term in an atomic infon term in infterm,or does not occur at all in infterm), then(<=> (infon (Q var infterm))(Q (var : (individual var)) (infon infterm)))).A.5.3Basic Situation Theoretic RelationsIn this section, the basic situation theoretic relations are introduced and, by means of definingaxioms, their legitimate argument types are declared.
Note that, as with the basic categories ofthe elaboration language core, “legitimate” here is understood semantically, and enforcedaxiomatically. Any terms whatsoever can be used to construct syntactically correct sentencesinvolving the relation terms introduced below. However, such sentences can be true only if theaxiomatized constraints are satisfied.(define-relation supports (?x ?y ?z)):=> (and (situation ?x) (infon ?y) (interval ?z)))(define-relation denies (?x ?y):=> (and (situation ?x) (infon ?y) (interval ?z)))(define-relation occurrence-of (?x ?y):=> (and (situation ?x) (UOB ?y)))(define-relation activation-of (?x ?y):=> (and (COE ?x) (process ?y)))(define-relation occurs-in (?x ?y):=> (and (situation ?x) (COE ?y)))(define-relation activity-in (?x ?y):=> (and (UOB ?x) (process ?y)))(define-relation of-type (?x ?y):=> (and (situation ?x) (UOB ?y)))(define-relation object-in (?x ?y)212:=> (and (individual ?x) (or (situation ?y) (UOB ?y)))A.5.4Basic Temporal RelationsIn this section, some basic temporal relations between intervals are introduced.
The onlyprimitive relation needed for characterizing the temporal intervals used in IDEF3 is the meetsrelation, which can be true only of intervals, as indicated in the following partial definition.(define-relation meets (?x ?y):=> (and (interval ?x) (interval ?y)))Intuitively, as noted, one temporal interval meets another just in case the end point of the firstis identical with the starting point of the second. A logic for the meets relation as found in (Allen& Hayes, 1987) is assumed [see also (van Bentham, 1983)].A variety of useful temporal relations can be defined in terms of meets. The first is stronglyprecedes, where one interval strongly precedes another just in case the first meets an interval thatmeets the second.(define-relation strongly-precedes (?x ?y):= (exists (?z ?w : (/= ?z ?w)) (and (meets ?x ?z) (meets ?z ?w) (meets ?w ?y))))Note that, because points are intervals, we need to put two distinct intervals between ?x and ?y.In fact, a point can be defined as an interval that meets itself (this is a divergence from Allen andHayes).(define-relation point (?x):= (meets ?x ?x))One temporal interval i starts another j just in case both are met by a given interval but j meets aninterval which is met by an interval met by i:(define-relation starts (?x ?y):= (exists ?z (and (meets ?z ?x) (meets ?z ?y)(exists ?w (and (meets ?y ?w) (strongly-precedes ?x ?w)))))Similarly, a temporal interval i finishes another j just in case both meet a given interval but i ismet by an interval that starts j:(define-relation finishes (?x ?y):= (exists (?z ?w : (starts ?w ?y)) (and (meets ?x ?z) (meets ?y ?z) (meets ?w ?x))))i overlaps j just in case some interval that finishes i starts j:(define-relation overlaps (?x ?y):= (exists ?z (and (finishes ?z ?x) (starts ?z ?y))))213i is during j just in case some interval that starts j meets i and i meets some interval thatfinishes j:(define-relation during (?x ?y):= (exists (?z ?w) (and (starts ?z ?y) (meets ?z ?x) (finishes ?w ?y) (meets ?x ?w)))Other useful relations can be defined in a similarly straightforward fashion.A.5.5The Interval Over Which a Situation OccursIt is very important in describing processes and their activations to be able to talk about theinterval of time over which a given situation occurs.
For this reason, a function is defined that,when applied to a given situation, yields exactly that interval:(define-function interval-of:=> (forall (?sit ?t)(=> (= interval-of ?sit) ?t)(and (situation ?sit) (interval ?t)))))Given the temporal relations, by defining the interval over which a situation occurs, a varietyof useful temporal relations among situations can be defined in terms of corresponding temporalrelations between the intervals over which they occur. See (Menzel & Mayer, forthcoming) fordetails.A.5.6Using Sorted VariablesNote that the IDEF3 elaboration language proper is completely untyped; in particular, there isonly one sort of variable. However, the informal examples shown in Section A.4 and in Section3 use a wide variety of sorted variables whose possible values are restricted to various semanticcategories—e.g., UOBs, situations, infons, etc. This practice can be viewed as simply aconvenient use of alternative notation, as any sentence in a so-called many-sorted language withmany different sorts of restricted variables can be translated directly into a sentence of a singlesorted language such as the elaboration language.
The trick is simply to use the terms in thesingle sorted language that denote the semantic categories to which the sorted variables arerestricted in the many-sorted language. For example, suppose “?sit” is a sorted variable rangingonly over situations and “?ind” is a sorted variable ranging only over individuals. Then thesentence “(forall (?sit ?ind : (FOO ?sit)) (BAR ?ind ?sit)))” says that, for any situation s andindividual b, if s is a FOO, then b bears BAR to s. Clearly, however, this can be expressed in thestrict, single-sorted elaboration language as “(forall (?x ?y : (situation ?x) (individual ?y) (FOO?x)) (BAR ?y ?x))”. The use of sorted variables is therefore innocuous, and indeed, encouraged,as their use typically decreases significantly the length of a sentence written in single sortednotation.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
