idef3_kbsi_report (1013870), страница 40
Текст из файла (страница 40)
Forinstance, in set theoretic treatments such as in KIF, a two-place relation is a set of ordered pairs,and a function is just a two-place relation; such that the first element of any given pair in therelation is not also paired with any other object. Formally, this identification is very convenient.Hence, this identification is added as a defining axiom for functions. Similarly, both intervalsand integers are taken to be kinds of individuals.The duality of functions, viewed as both functions and relations, is captured in the followingseries of axioms.Two objects stand in the (binary) functional relation f iff the value of f applied to the firstobject is the second.(forall (?x ?y ?f : (function ?f)) (<=> (?f ?x ?y) (= (?f ?x) ?y))))Three objects stand in the (ternary) functional relation f iff the value of f on the first twoobjects is the third.(forall (?x ?y ?z ?f : (function ?f)) (<=> (?f ?x ?y ?z) (= (?f ?x ?y) ?z))))In general, we have the following axiom schema:(forall (?var1 .
. . ?varn+1 ?f : (function ?f))203(<=> (?f ?var1 . . . ?varn+1) (= (?f var1 . . . ?varn) ?varn+1))))A.3.1.2ArityThe arity of a function or relation indicates how many arguments it takes. Because functionsare also relations, two separate notions of arity are required: rel-arity and func-arity.
rel-arity isa function that takes a relation as an argument and yields a positive integer as its value.(define-function rel-arity(forall (?x ?y : (/= ?y null))(=> (= (arity ?x) ?y)(and (relation ?x) (integer ?y) (> ?y 0)))))Let the lower case Greek letter “n” be the numeral for the number n. The following axiomschema expresses the connection between the rel-arity of a relation and the truth of an atomicsentence involving a term referring to that relation, viz., in essence: An atomic sentence can betrue only if it consists of a relation of arity n followed by n terms.(forall(?r ?var1 .
. . ?varn)(=> (?r ?var1 . . . ?varn)(and (relation ?r) (= (arity ?r) n).Note that this cannot be expressed by quantifying over numbers with a variable ?n insteadusing the schematic letter n, as the schematic expression “(?r ?var1 . . . ?varn)” is not anexpression in the elaboration language proper.Analogous to rel-arity, func-arity is a function that takes a function as an argument and yieldsa positive integer as its value.(define-function func-arity(forall (?x ?y : (/= ?y null))(=> (= (arity ?x) ?y)(and (function ?x) (integer ?y) (> ?y 0)))))The connection between the func-arity of a function the denotation of a function terminvolving a term referring to that function is captured in the following axiom schema, whichsays, in essence, that: An atomic function term that does not denote the null object must consistof an n-place function followed by n terms.(forall (?f ?var1 . .
. ?varn: (=/ (?f ?var1 . . . ?varn) null)))(and (function ?f) (= arity ?f n)))The following axioms put further constraints on the arity functions.All relations and functions have a (non-null) arity.204(forall ?x (=>(or (relation ?x) (function ?x))(/= (arity ?x) null)))Because every function is a relation, both rel-arity and func-arity are defined on functions.There is, of course, a close relationship between them, viz.,, if f is viewed as a function, funcarity yields one value on f, and viewed as a relation, rel-arity yields another; more exactly, as thefollowing axiom states,The rel-arity of a function is one greater than its func-arity.(forall (?f : (function ?f)) (= (rel-arity ?f) (+ (func-arity ?f) 1)))An atomic sentence consisting of an n-place relation and some number of argument termsother than n must be false:(forall (?var1 .
. . ?varn ?r : (relation ?r) (= (arity ?r) m))(not (?r ?var1 . . . ?varn))), where m is not the numeral for n.A function term consisting of an n-place function term and some number of argument termsother than n must denote the null object:(forall (?f ?var1 . . . ?varn: (function ?f) (= (arity ?f) m))(= (?f ?var1 .
. . ?varn) null))), where m is not the numeral for n.A.3.1.2The Null ObjectThe following two axiom schemas characterize the null object and its connections withfunctions and relations.An atomic sentence that contains a term denoting the null object must be false:(forall (?r ?var1 . . . ?varn : (relation ?r) (or (= ?var1 null) . . . (= ?varn null)))(not (?r ?var1 . .
. ?varn)))A function term that includes a term denoting the null object must itself denote the nullobject:(forall (?f ?var1 . . . ?varn : (function ?f) (or (= ?var1 null) . . . (= ?varn null)))(= (?f ?s1 . . . ?sn) null))A.4Basic Situation TheoryThe underlying intuitive semantics for both process schematics and state transitionschematics is based upon situation theory. The purpose of the IDEF3 elaboration language is topermit very precise expression of additional constraints and other information about a given205process or state transition.
The core elaboration language is extended with situation theoreticconstructs tailored specifically for IDEF3. The theory implicit in these constructs is somewhatless powerful than some versions of full-blown situation theory, but, in addition to a clear,intuitive semantics, experience has shown that this theory is all that is needed for most allenterprise process capture and modeling. In the following sections, a brief overview of situationtheory is provided to guide the reader in formulating elaboration statements in the elaborationlanguage.A.4.1Situations and InfonsThe notion of a situation is the most fundamental notion of situation theory.
This notion isfamiliar in the literature of knowledge representation. Situations are (typically) concrete,spatially and temporally extended pieces of the real world, such as a baseball game, a math class,a manufacturing system (though situations in nonconcrete systems are admitted as well; e.g., thefield of real numbers). In situation theory, what distinguishes a given situation from any otherare the pieces of information it supports, or that hold in it. In situation theory, individual piecesof information are known as infons.
The infons in a given domain are themselves constituted byobjects, properties, and relations that exist in the domain. (Objects here are construed broadly toinclude not only physical objects, but also abstract ones like numbers and intervals of time.)More specifically, the basic infons in a given situation s are the fundamental units of information,good and bad, “generated” combinatorially from the relations and appropriate arguments forthose relations within s; that is, the basic infons of s consist of all possible legitimate units ofinformation of the formobjects a1, ..., an stand in relation r,andobjects a1, ..., an do not stand in relation r,where r and the ai are all constituents of s.
(Relations that hold among individual objects areknown as first-order relations.) These infons will be represented in the language that will bedeveloped here as “(r a1 ..., an +)” and “(r a1 ..., an -)”, respectively. A situation s supports a basic“positive” infon (r a1 ..., an +) just in case its component objects a1, ..., an are present in s (at leastat some time during s) and stand in the relation r in s, and s supports a basic “negative” infon (r a1... an –) just in case a1, ..., an are present in s but do not stand in that relation in s.
s denies(r a1 ... an +) just in case its component objects a1, ..., an are present in s but do not stand in therelation r in s, and s denies (r a1 ... an –) just in case a1, ..., an are present in s but do stand in therelation r in s. Thus, for example, the infons (mother-of Hillary Chelsea +) and (mother-ofChelsea Hillary –) are supported by, or hold in, typical White House situations s in 1995; bycontrast, such situations deny (mother-of Chelsea Hillary +) and (mother-of Hillary Chelsea –); wealso say that these infons fail in such situations. In the language here, these facts would beexpressed as “(supports s (mother-of Hillary Chelsea +))”, “(supports s (mother-of ChelseaHillary –))”, “(denies s (mother-of Hillary Chelsea -))” and “(denies s (mother-of Chelsea Hillary+)), respectively, where s is an appropriate White House situation.206Note that, because situations are (in general) limited pieces of the world, an object b thatexists in one situation s may not exist in another s¢.
Hence, s¢ will be “silent” on b; moreexactly, it will support no information about b. Situations are partial with respect toinformation; they do not answer every question about every individual or every state of affairs.A typical baseball game in the Houston Astrodome, for example, carries no information about,say, the price of Coho salmon in Seattle’s Pike Place Market.To say that s supports a given basic infon (r a1 ... an +) is to say that the individuals a1, ..., anstand in the relation r throughout s. However, things can change within a situation—e.g., onechanges from sleeping to waking in typical morning situations.















