In this section we extend Positive Conditions, defined in Section Positive Conditions, with *slotted Uniterm*s 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.

## Syntax

### Abstract Syntax

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

class CONDITION 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 CLASSIFICATION subclass Frame class TERM subclass Var property name: xsd:string subclass Const property name: xsd:string subclass Uniterm property op: Const property subproperty arg: list of TERM subproperty slot: list of list Const TERM class CLASSIFICATION subclass Instance property oid: TERM property op: TERM subclass Subclass property sub: TERM property op: TERM class Frame property subproperty oid: TERM subproperty classinst: CLASSIFICATION property slot: list of list TERM TERMFRAME class 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 `TERM`s are just `list`ed). 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 `slot`s, 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.

CONDITION ::= CONJUNCTION | DISJUNCTION | EXISTENTIAL | ATOMIC CONJUNCTION ::= 'And' '(' CONDITION* ')' DISJUNCTION ::= 'Or' '(' CONDITION* ')' EXISTENTIAL ::= 'Exists' Var+ '(' CONDITION ')' ATOMIC ::= Uniterm | Equal | CLASSIFICATION | Frame Uniterm ::= Const '(' TERM* ')' | Const '(' (Const '->' TERM)* ')' CLASSIFICATION ::= TERM '#' TERM | TERM '##' 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)) Frames: 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 seller->?Seller item->book{author->?Author title->LeRif} price->$49]) ?Seller=?Author ) b. XML serialization: <And> <formula> <Exists> <declare><Var>Buyer</Var></declare> <declare><Var>P</Var></declare> <formula> <Frame> <classinst> <Instance> <oid><Var>P</Const></Var> <op><Const>purchase</Const></op> </Instance> </classinst> <slot><Const>buyer</Const><Var>Buyer</Var></slot> <slot><Const>seller</Const><Var>Seller</Var></slot> <slot> <Const>item</Const> <Uniterm> <op><Const>book</Const></op> <slot><Const>author</Const><Var>Author</Var></slot> <slot><Const>title</Const><Const>LeRif</Const></slot> </Uniterm> </slot> <slot><Const>price</Const><Const>$49</Const></slot> </Frame> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And>

## Semantics

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

*is a formula that is always true (a tautology, a formula whose truth value is*

**true***). If*

**t**`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*,

*, is now a tuple of the form*

**I**<

,**D****I**_{C},**I**_{V},**I**_{F},**I**_{R},**I**_{slot},**I**_{SR},**I**_{sub},**I**_{isa}>.

All the components except the last four, **I**_{slot}, **I**_{SR}, **I**_{sub}, **I**_{isa}, are the same as before. The new mapping **I**_{slot} is used to interpret frames; the mapping **I**_{SR} interprets predicates with named arguments; **I**_{sub} i gives meaning to the subclass hierarchy; and **I**_{isa} interprets class membership.

**I**_{slot}is a function formto truth-valued functions of the form**D**×**D**→**D**. The intuitive meaning of frame slots is that they are functions that take objects and return**TV***sets*of objects, where every member of the set has certain degree of truth. In the two-valued case, a set of objects associated with the truth value*true*represents the (set of) values that the slot returns when applied to an object. Formally, this is expressed by extending**I**_{Truth}to flat frames as follows:**I**_{Truth}(`T[slot`_{1}`->V`_{1}`... slot`_{k}`->V`_{k}`]`) = min_{i=1...k}(**I**_{Truth}(`T[slot`_{i}`->V`_{i}`]`)), where`T`,`slot`_{i}, and`V`_{i}are terms.**I**_{Truth}(`T[slot`_{i}`->V`_{i}]) =**I**_{slot}((**I**`slot`_{i}))((**I**`T`),(**I**`V`))

**I**_{SR}is used to interpret predicates with slotted arguments. It is a function from`Const`to truth-valued mappings`SetOfFiniteSubbags`(×**D**) →**D**. This is analogous to the interpretation of regular (positional) predicates except for two differences:**TV**-- Each pair

`<s,v>`∈×**D**represents a slot-value pair instead of just a value in positional predicates. -- A tuple in a slotted predicate is a finite bag of slot-value pairs rather than an ordered sequence.**D**Bags are used here because for slotted predicates the order of slot-value pairs does not matter, but sets cannot be used, since

may happen to map different slots into the same value in**I**.**D**

We can now define

**I**_{Truth}for slotted predicates as follows:**I**_{Truth}(p(`slot`_{1}`->val`_{1}...`slot`_{k}`->val`_{k})) =**I**_{SR}(p)(`<`(**I**`slot`_{1})(**I**`val`_{1})`>`, ... ,`<`(**I**`slot`_{k})(**I**`val`_{k})`>`), where`p`∈`Const`, and`slot`_{i}and`val`_{i}are terms.

**I**_{sub}gives meaning to the subclass relationship. It is a truth-valued function×**D**→**D**. For the two valued case,**TV****I**_{sub}is required to define a partial order on. More precisely, the set of all pairs**D**`<a,b>`such that(**I**`<a,b>`) =**t**is required to be a partial order on. When**D**is multivalued, the restriction on**TV****I**_{sub}will depend on the corresponding multivalued logic. The truth valuation for classification formulas of the form`sc##cl`, where`sc`and`cl`are terms, is defined as follows:**I**_{Truth}(`sc##cl`) =**I**_{sub}((**I**`sc`),(**I**`cl`))

**I**_{isa}gives meaning to class membership. It is a truth-valued function×**D**→**D**. The truth valuation for classification formulas of the form**TV**`o#cl`, where`o`and`cl`are terms, is defined as follows:**I**_{Truth}(`o#cl`) =**I**_{isa}((**I**`o`),(**I**`cl`))

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