This is an archive of an inactive wiki and cannot be modified.

In this section we extend Positive Conditions, defined in Section Positive Conditions, with slotted Uniterms and Frame formulas. A slot can be represented by an individual symbol or, more generally, by a Uniterm. It can be represented by an IRI or be known only locally. Semantically, a frame slot is a set-valued binary function that represents a property of an object. Such a function maps an object id to a value (or a set of values) of the property. In contrast, a uniterm slot semantically behaves like a unary function symbol. In both cases, however, the order of the slots is immaterial (in contrast to positional uniterms).

Syntactically, the extension is achieved by enriching the notion of a uniterm with slots and by complementing these with frame formulas. For uniformity and greater syntactic convenience, frame formulas can be nested inside other frame formulas. This is syntactic sugar, however, as explained later in this section.


Abstract Syntax

The abstract syntax of the slotted condition language is given in asn06 as follows:


    subclass And
        property formula : list of CONDITION

    subclass Or
        property formula : list of CONDITION

    subclass Exists
        property declare : list of Var
        property formula : CONDITION

    subclass ATOMIC

class ATOMIC

    subclass Equal
       property side: list TERM TERM

    subclass Uniterm


    subclass Frame

class TERM

    subclass Var
        property name: xsd:string

    subclass Const
        property name: xsd:string

    subclass Uniterm
        property op: Const
            subproperty arg: list of TERM
            subproperty slot: list of list Const TERM


          subclass Instance
              property oid: TERM
              property op: TERM

          subclass Subclass
              property sub: TERM
              property op: TERM

class Frame
       subproperty oid: TERM
       subproperty classinst: CLASSIFICATION
   property slot: list of list TERM TERMFRAME


    subclass TERM

    subclass Frame

The above asn06 is generalized with a fixed-arity list constructor (complementing the unfixed-arity list of constructor) so that the multiplicity of the side property (role) of the Equal class no longer requires the assumption of being exactly 2 (the 2 TERMs are just listed). This also allows the name and filler of a slot to be defined as a sequence of two classes. Since no set of constructor is available, list of is used to represent a set of slots, assuming that duplicates and order will not matter. Also, optional of and subproperty constructs are assumed.

The abstract syntax is visualized by a UML diagram used as a schema-level device for specifying syntactic classes with generalizations as well as multiplicity- and role-labeled associations. (***TBD***)

Upload new attachment "SlottedConditionModel.png"

The syntactic classes are partitioned into classes that will not be visible in serializations (written in all-uppercase letters) and classes that will be visible in instance markup (written with a leading uppercase letter only).

The three classes Var, CONDITION, and ATOMIC will be required in the abstract syntax of Horn Rules.

Concrete Syntax

The abstract syntax of Section Abstract Syntax can be instantiated to a concrete syntax which is an extension to the concrete syntax of Positive Conditions for slotted Uniterms. The EBNF syntax below, which instantiates the abstract syntax, is used throughout this document to explain and illustrate the main ideas.

The concrete human-readable syntax, described in this (slightly modified) EBNF, is work in progress and under discussion.

  CONJUNCTION    ::= 'And' '(' CONDITION* ')'
  DISJUNCTION    ::= 'Or' '(' CONDITION* ')'
  EXISTENTIAL    ::= 'Exists' Var+ '(' CONDITION ')'
  ATOMIC         ::= Uniterm | Equal | CLASSIFICATION | Frame
  Uniterm        ::= Const '(' TERM* ')' | Const '(' (Const '->' TERM)* ')'
  Frame          ::= (TERM | CLASSIFICATION) '[' (TERM '->' (TERM | Frame))* ']'
  Equal          ::= TERM '=' TERM
  TERM           ::= Const | Var | Uniterm
  Const          ::= CONSTNAME | '"'CONSTNAME'"''^^'SORTNAME
  Var            ::= '?'VARNAME | '?'VARNAME'^^'SORTNAME

A Uniterm ()-applies a Const to positional TERM arguments or to slotted Const -> TERM arguments. A CLASSIFICATION #-associates a TERM with a typing class TERM, or ##-associates a TERM with a superclass TERM. A Frame []-applies a TERM or a CLASSIFICATION to slotted TERM -> (TERM | Frame) arguments.

Example 1 shows Uniterm and Frame conditions, the latter with variables for the three major (combinations of) syntactic categories, corresponding to the three components of RDF triples.

Example 1 (A RIF condition with bound variables)

RIF conditions using

   Positional Uniterms:
                        book(rifwg LeRif)

                        Exists ?X (book(?X LeRif))

   Slotted Uniterms:
                        book(author->rifwg title->LeRif)

                        Exists ?X (book(author->?X title->LeRif))

                        wd1[author->rifwg title->LeRif]

                        Exists ?X (wd1[author->?X title->LeRif])

                        Exists ?X (wd1#book[author->?X title->LeRif])

                        Exists ?I ?X (?I[author->?X title->LeRif])

                        Exists ?I ?X (?I#book[author->?X title->LeRif])

                        Exists ?S (wd1[author->rifwg ?S->LeRif])

                        Exists ?X ?S (wd1[author->?X ?S->LeRif])

                        Exists ?I ?X ?S (?I#book[author->?X ?S->LeRif])

The following is a possible XML-serializing mapping of the abstract syntax in Section Abstract Syntax (and of the above EBNF syntax).

- And       (conjunction)
- Or        (disjunction)
- Exists    (quantified formula for 'Exists', containing declare and formula roles)
- declare   (declare role, containing a Var)
- formula   (formula role, containing a CONDITION formula)
- Uniterm   (positional or slotted Uniterm formula)
- Instance  (instance-of formula)
- Subclass  (subclass-of formula)
- Frame     (slotted Frame formula)
- classinst (Frame role for Subclass or Instance)
- oid       (Instance/Frame identifier role, containing a TERM)
- op        (Uniterm/Instance/Subclass predicate/class role)
- sub       (Subclass role for included class)
- slot      (Uniterm/Frame slot role, prefix version of slot infix '->')
- Equal     (prefix version of term equation '=')
- Const     (slot, individual, function, or predicate symbol)
- Var       (logic variable)

The following example illustrates XML serialization of Slotted RIF conditions.

Example 2 (A RIF condition and its XML serialization):

a. RIF condition:

  And ( Exists ?Buyer ?P (?P#purchase[buyer->?Buyer
                                      item->book{author->?Author title->LeRif}
        ?Seller=?Author )

b. XML serialization:



The syntax of RIF frames permits nesting of two kinds. First, a classification formula of the form obj1#obj2 or obj1##obj2 can appear in the object position of a frame. Second, a frame may appear in the value position of an attribute. This nested notation is convenient and allows succinct representation of object properties, but is no more than a shorthand notation. A nested frame represents a conjunction of flat frames. For instance,

   a#b[c -> e##f[g -> h]]    ==    a#b /\ a[c -> e] /\ e##f /\ e[g -> h]

Formally, we define the Unnest transformation and postulate that for any frame, f, it is true in a semantic structure iff Unnest(f) is true. In this way, we reduce the semantics of nested frames to that of flat frames. Then we extend the semantic structures defined in Semantics of the Multisorted RIF Conditions and define an interpretation for flat frames. The rest of the semantic definitions does not change, since it is defined in terms of atomic formulas (the ATOMIC production in the BNF syntax).

The Unnest Transformation

If a formula, f, has the form a#b or a##b then define Obj(f) to be a. If f has the form o[a->v], where o, a, and v are terms, then Obj(f) is defined to be Obj(o). Now, if f is a uniterm then we define Unnest(f) = true, where true is a formula that is always true (a tautology, a formula whose truth value is t). If f is a classification formula then Unnest(f) = f. Otherwise, if f is a frame of the form o[a->v] then

   Unnest(f) = Unnest(o) /\ Obj(o)[a -> Obj(v)] /\ Unnest(v)

For instance, in case of the frame a#b[c->e##f[g->]] above, unnesting yields:

   Unnest(a#b[c -> e##f[g -> h]])    =    a#b /\ a[c -> e] /\ e##f /\ e[g -> h] /\ true

This is almost the same conjunction as we have seen earlier. The only difference is the trailing true, which comes from Unnest(h) and can be omitted.

Extension of Semantic Structures for Frames

A semantic structure, I, is now a tuple of the form

All the components except the last four, Islot, ISR, Isub, Iisa, are the same as before. The new mapping Islot is used to interpret frames; the mapping ISR interprets predicates with named arguments; Isub i gives meaning to the subclass hierarchy; and Iisa interprets class membership.

MK: ***** The effect of sorts on all this stuff is to be filled in at a later time ********