RIF Core

1 Overview

2 Direct Specification ofRIF-Core Presentation Syntax

2.1 Alphabet of RIF-Core

The Condition Language represents formulas that can be used inalphabet of the premisespresentation language of RIF-Core rules (also called rule bodies).is the EBNF grammar for a supersetalphabet of the RIF-Core conditionRIF-BLD presentation language is as follows. Editor's Note: Stylistic comment only. Please could we just have one section forwith the combined condition and rule languageexclusion of the symbol ## and just talk aboutthe set of symbols ArgNames.

ISSUE: Did we really decide that ## cannot occur at all or that it can occur only in the rule language?bodies?

2.2 Terms of RIF-Core

The valueTerms of separating outRIF-Core are the condition language for reuse seems to primarily apply to FLD. Separating condition/rule syntax makes it harder to read and duplicatingterms of RIF-BLD with the condition part afterexclusion of terms with named arguments, subclass terms, and external terms of the rule partform External(fr), where fr is not entirely satisfying. Dave FORMULA ::= IRIMETA? 'And' '(' FORMULA* ')' | IRIMETA? 'Or' '(' FORMULA* ')' | IRIMETA? 'Exists' Var+ '(' FORMULA ')' | ATOMIC | IRIMETA? 'External' '(' Atom | Frame ')' ATOMIC ::= IRIMETA? (Atom | Member | Subclass | Frame) Atom ::= UNITERM UNITERM ::= Const '(' (TERM* | (Name '->' TERM)*) ')' Member ::= TERM '#' TERM Subclass ::= TERM '##' TERMa frame ::= TERM '[' (TERM '->' TERM)* ']' TERM ::= IRIMETA? (Const | Var) Const ::= '"' UNICODESTRING '"^^' SYMSPACE | CONSTSHORT Name ::= UNICODESTRING Var ::= '?' UNICODESTRING SYMSPACE ::= ANGLEBRACKIRI | CURIE IRIMETA ::= '(*' IRICONST? (Frame | 'And' '(' Frame* ')')? '*)'term.

Editor's Note: There was concern over disjunction and NAU, weaker concern over member and subclass. So a conservative versionThis presumes that the At Risk #1 feature External frames is as below. I realize you did qualifyretained in RIF-BLD. If that is not the case the above will need updating.

2.3 Formulas of RIF-Core

The Formulas of the RIF-Core are the formulas of RIF-BLD with the following modifications.

• The subterms that occur inside the ENBF as a superset . Dave: FORMULA ::= IRIMETA? 'And' '(' FORMULA* ')' | IRIMETA? 'Exists' Var+ '(' FORMULA ')' |atomic | IRIMETA? 'External' '(' Atom ')' ATOMIC ::= IRIMETA? (Atom | Frame) Atom ::= UNITERM UNITERM ::= Const '(' (TERM* ')' Frame ::= TERM '[' (TERM '->' TERM)* ']'formulas can be either variables or constants. This implies that RIF-Core does not allow function symbols in its formulas.
• Equality terms cannot occur in rule conclusions -- they are allowed only in rule premises.

ISSUE: What was decided about external functions?

2.4 Annotations and documents

RIF-Core allows every term ::= IRIMETA? (Const | Var) Const ::= '"' UNICODESTRING '"^^' SYMSPACE | CONSTSHORT Name ::= UNICODESTRING Var ::= '?' UNICODESTRING SYMSPACE ::= ANGLEBRACKIRI | CURIE IRIMETA ::= '(*' IRICONST? (Frame | 'And' '(' Frame* ')')? '*)'and formula to be optionally annotated in the production rule forsame way as RIF-BLD. The non-terminal FORMULA represents RIF conditionframe formulas (defined earlier). The connectives And and Or define conjunctions and disjunctionsthat are allowed as part of conditions, respectively. Exists introduces existentially quantified variables. Here Var+ standsan annotation must be syntactically correct for the list of variables thatRIF-Core. In particular, no function symbols are freeallowed in FORMULA . RIF-Core conditions permit only existential variables.such a formula.

2.5 Well-formed formulas

A syntactically correct RIF-Core formula canthat passes the well-formedness test for RIF-BLD is also a well-formed RIF-Core formula. In this case, it simply means that

2.6 EBNF Grammar for the Rule Language ThePresentation Syntax forof RIF-Core rules extends(Informative)

Until now, we have used mathematical English to specify the syntax of RIF-Core as a restriction on RIF-BLD. Tool developers, however, may prefer EBNF notation, which provides a more succinct overview of the syntax. However, note that EBNF is unable to express all of the above well-formedness conditions, in particular the requirement that each symbol appear in only one context. For this reason this section is not Normative.

The EBNF for the RIF-Core Condition Language withpresentation syntax is given as follows, showing the following productions.entire (top-down) context of its three parts for rules, conditions, and annotations.

Rule Language:

  Document      ::= IRIMETA? 'Document' '(' Base? Prefix* Import* Group? ')'
  Base          ::= 'Base' '(' IRI ')'
  Prefix        ::= 'Prefix' '(' Name IRI ')'
  Import        ::= IRIMETA? 'Import' '(' IRICONST PROFILE? ')'
  Group         ::= IRIMETA? 'Group' '(' (RULE | Group)* ')'
  RULE          ::= (IRIMETA? 'Forall' Var+ '(' CLAUSE ')') | CLAUSE
  CLAUSE        ::= Implies | ATOMIC
  Implies       ::= IRIMETA?  (ATOMIC | 'And' '(' ATOMIC* ')')ATOMIC  ':-' FORMULA
  PROFILE       ::= TERM

Editor's Note: PRD only permits Atom and Frame in the head so if member/subclass are retained in ATOMIC this needs modification. PRD/BLD syntactic intersection currently only works for one ASSERT in head, not with And. So PRD compatible version seems be as below. Dave DocumentCondition Language:

  FORMULA       ::= IRIMETA?  'Document' '(' Base? Prefix* Import* Group? ')' Base ::= 'Base' '(' IRI ')' Prefix ::= 'Prefix''And' '('  Name IRIFORMULA* ')'  Import ::=|
                     IRIMETA?  'Import''Or' '('  IRICONST PROFILE?FORMULA* ')'  Group ::= IRIMETA? 'Group' '(' (RULE|
                      Group)* ')' RULE ::= (IRIMETA? 'Forall'IRIMETA? 'Exists' Var+ '('  CLAUSE ')')FORMULA ')' |
                      CLAUSE CLAUSE ::= ImpliesATOMIC |
                     IRIMETA? Equal |
                     IRIMETA? Member |
                     IRIMETA? 'External' '(' Atom ')'
  ATOMIC         Implies::= IRIMETA? (Atom | Frame )
   ':-' FORMULA PROFILEAtom          ::= UNITERM
  UNITERM       ::= Const '(' (TERM* ')'
  Equal         ::= TERM  Recall that an IRI has'=' TERM
  Member        ::= TERM '#' TERM
  Frame         ::= TERM '[' (TERM '->' TERM)* ']'
  TERM          ::= IRIMETA? (Const | Var  | 'External' '(' Atom ')' )
  Const         ::= '"' UNICODESTRING '"^^' SYMSPACE | CONSTSHORT
  Name          ::= UNICODESTRING
  Var           ::= '?' UNICODESTRING
  SYMSPACE      ::= ANGLEBRACKIRI | CURIE

Annotations:

  IRIMETA       ::= '(*' IRICONST? (Frame | 'And' '(' Frame* ')')? '*)'

The form of an internationalized resource identifier as defined by [ RFC-3987 ]. A RIF-Core Document consists of an optional Base , followed by any number of Prefix es, followed by any number of Import s, followed by an optional Group . Basefollowing subsections explain and Prefix serve as shortcut mechanisms for IRIs. An Import indicatesexemplify the location of a document to be importedCondition Language and an optional profile. A RIF-Core Group is a collection of any number of RULE elements along with any number of nested Group s. Rules are generated using CLAUSE elements. TheRule production has two alternatives: InLanguage parts; the first, a CLAUSEAnnotations part is inunchanged from RIF-BLD.

2.6.1 EBNF for the scope ofRIF-Core Condition Language

2.6.2 EBNF for the scheduled delivery date thenRIF-Core Rule Language

3 RIF-Core Semantics

RIF-Core is a syntactic subset of RIF-BLD and the firstsemantics of these rulesRIF-Core is copied from Example 3a.identical that of RIF-BLD.

4 XML Serialization Syntax for RIF-Core

5 Conformance and Safety

RIF-Core is a syntactic subset of both RIF-BLD and RIF-PRD. The imagesemantics of a well-formedRIF-Core document in the presentation syntax (see Definition Well-formedformula is the same as in SectionRIF-BLD.

5.1 Safeness

A subformula of RIF-Core in Section EBNF fora RIF-Core condition Language uses the following elements. - 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 FORMULA) - Atom (atom formula, positional or with named arguments) -is called an external (external call, containing a content role) - content (content role, containingsubformula if it appears within an Atom) - Member (member formula) - Subclass (subclass formula) - Frame (Frame formula) - object (Member/Frame role, containingExternally defined term. A TERM or an object description) - op (Atom role for predicates/functions as operations) - args (Atom positional arguments role, with fixed 'ordered' attribute, containing n TERMs) - instance (Member instance role) - class (Member class role) - sub (Subclass sub-class role) - super (Subclass super-class role) - slot (Atom or Frame slot role, with fixed 'ordered' attribute, containingsubformula of a Name or TERM followed bycondition formula is called disjunctive subformula if it appears within a TERM) - Const (individual, function, or predicate symbol, with optional 'type' attribute) - Name (name of named argument) - Var (logic variable) - id (identifier role, containing IRICONST) - meta (meta role, containing metadata asDisjunction.

Definition (Safeness).

• A Frame or Frame conjunction) The id and meta elements, which are expansions of the IRIMETA element, can occur optionally as the initial children of any Class element. For the XML Schema definition of the RIF-Core condition language see Appendix XML Schema for Core . The XML syntax for symbol spaces uses the type attribute associated with the XML element Const . For instance, a literal in the xs:dateTime datatype is represented as <Consttype="&xs;dateTime">2007-11-23T03:55:44-02:30</Const> . RIF-Core also uses the ordered attribute to indicate that the children of args and slot elements are ordered. Example 5 (A RIF condition and its XML serialization). This example illustrates XML serialization for RIF conditions. As before, the compact URI notationvariable ?v is used for better readability. Assume that the following prefix directives are found in the preamblecalled safe with respect to the document: Prefix(bks http://example.com/books#) Prefix(cpt http://example.com/concepts#) Prefix(curr http://example.com/currencies#) Prefix(rif http://www.w3.org/2007/rif#) Prefix(xs http://www.w3.org/2001/XMLSchema#)a RIF condition And (Exists?Buyer (cpt:purchase(?Buyer ?Seller cpt:book ?Author bks:LeRif curr:USD 49)) pred:string-equal(?Seller?Author) ) *** ED Note in DTB 4.5.1.1. Add pred Prefix. Or: Replace?Seller with?Author *** XML serialization *** TBD as in PS *** <And> <formula> <Exists> <declare><Var>Buyer</Var></declare> <formula> <Atom> <op><Const type="&rif;iri">&cpt;purchase</Const></op> <args ordered="yes"> <Var>Buyer</Var> <Var>Seller</Var> <Expr> <op><Const type="&rif;iri">&cpt;book</Const></op> <args ordered="yes"> <Var>Author</Var> <Const type="&rif;iri">&bks;LeRif</Const> </args> </Expr> <Expr> <op><Const type="&rif;iri">&curr;USD</Const></op> <args ordered="yes"><Const type="&xs;integer">49</Const></args> </Expr> </args> </Atom> </formula> </Exists> </formula> <formula> <Equal> <left><Var>Seller</Var></left> <right><Var>Author</Var></right> </Equal> </formula> </And> Example 6 *** TBD *** 4.2 XML for the Rule Language We now extend the set of RIF-Core serialization elements from Section XML for RIF-Core Condition Language by including rules, along with their enclosing groups and documents, as described in Section EBNF for RIF-Core Rule Language . The extended set includes the tags listed below. While there is a RIF-Core element tag for the Import directive, there are none for the Prefix and Base directives: they are handled as discussed in Section Mapping of the RIF-Core Rule Language . - Document (document, containing optional directive and payload roles) - directive (directive role, containing Import) - payload (payload role, containing Group) - Import (importation, containing location and optional profile) - location (location role, containing IRICONST) - profile (profile role, containing PROFILE) - Group (nested collection of sentences) - sentence (sentence role, containing RULE or Group) - Forall (quantified formula for 'Forall', containing declare andformula roles) - Implies (implication, containing if and then roles) -if (antecedent role, containing FORMULA) - then (consequent role, containing ATOMIC or conjunction of ATOMICs) The XML Schema Definition of RIF-Core is given in Appendix XML Schema for Core . Example 7 (Serializing a RIF-Core document containing an annotated group). This example shows a serialization for the document from Example 4. For convenience, the document is reproduced at the top and then is followed by its serialization. Presentation syntax: Document( Prefix(ppl http://example.com/people#) Prefix(cpt http://example.com/concepts#) Prefix(dc http://purl.org/dc/terms/) Prefix(func http://www.w3.org/2007/rif-builtin-function#) Prefix(pred http://www.w3.org/2007/rif-builtin-predicate#) Prefix(xs http://www.w3.org/2001/XMLSchema#) (* "http://sample.org"^^rif:iri pd[dc:publisher -> http://www.w3.org/ dc:date -> "2008-04-04"^^xs:date] *) Group ( Forall?item?deliverydate?scheduledate?diffduration?diffdays ( cpt:reject(ppl:John?item):- And(cpt:perishable(?item) cpt:delivered(?item?deliverydate ppl:John) cpt:scheduled(?item?scheduledate) ***replace with equality-less version***?diffduration = External(func:subtract-dateTimes(?deliverydate?scheduledate)) ***replace with equality-less version***?diffdays = External(func:days-from-duration(?diffduration)) External(pred:numeric-greater-than(?diffdays 10))) ) Forall?item ( cpt:reject(ppl:Fred?item):- cpt:unsolicited(?item) ) ) ) XML syntax: *** TBD as in PS *** <!DOCTYPE Document [ <!ENTITY ppl "http://example.com/people#"> <!ENTITY cpt "http://example.com/concepts#"> <!ENTITY dc "http://purl.org/dc/terms/"> <!ENTITY rif "http://www.w3.org/2007/rif#"> ***???***<!ENTITY func "http://www.w3.org/2007/rif-builtin-function#"> <!ENTITY pred "http://www.w3.org/2007/rif-builtin-predicate#"> <!ENTITY xs "http://www.w3.org/2001/XMLSchema#"> ]> <Document xmlns="http://www.w3.org/2007/rif#" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xs="http://www.w3.org/2001/XMLSchema#"> <payload> <Group> <id> <Const type="&rif;iri">http://sample.org</Const> </id> <meta> <Frame> <object> <Const type="&rif;local">pd</Const> </object> <slot ordered="yes"> <Const type="&rif;iri">&dc;publisher</Const> <Const type="&rif;iri">http://www.w3.org/</Const> </slot> <slot ordered="yes"> <Const type="&rif;iri">&dc;date</Const> <Const type="&xs;date">2008-04-04</Const> </slot> </Frame> </meta> <sentence> <Forall> <declare><Var>item</Var></declare> <declare><Var>deliverydate</Var></declare> <declare><Var>scheduledate</Var></declare> <declare><Var>diffduration</Var></declare> <declare><Var>diffdays</Var></declare> <formula> <Implies> <if> <And> <formula> <Atom> <op><Const type="&rif;iri">&cpt;perishable</Const></op> <args ordered="yes"><Var>item</Var></args> </Atom> </formula> <formula> <Atom> <op><Const type="&rif;iri">&cpt;delivered</Const></op> <args ordered="yes"> <Var>item</Var> <Var>deliverydate</Var> <Const type="&rif;iri">&ppl;John</Const> </args> </Atom> </formula> <formula> <Atom> <op><Const type="&rif;iri">&cpt;scheduled</Const></op> <args ordered="yes"> <Var>item</Var> <Var>scheduledate</Var> </args> </Atom> </formula> <formula> <Equal> <left><Var>diffduration</Var></left> <right> <External> <content> <Expr> <op><Const type="&rif;iri">&func;subtract-dateTimes</Const></op> <args ordered="yes"> <Var>deliverydate</Var> <Var>scheduledate</Var> </args> </Expr> </content> </External> </right> </Equal> </formula> <formula> <Equal> <left><Var>diffdays</Var></left> <right> <External> <content> <Expr> <op><Const type="&rif;iri">&func;days-from-duration</Const></op> <args ordered="yes"> <Var>diffduration</Var> </args> </Expr> </content> </External> </right> </Equal> </formula> <formula> <External> <content> <Atom> <op><Const type="&rif;iri">&pred;numeric-greater-than</Const></op> <args ordered="yes"> <Var>diffdays</Var> <Const type="&xs;integer">10</Const> </args> </Atom> </content> </External> </formula> </And> </if> <then> <Atom> <op><Const type="&rif;iri">&cpt;reject</Const></op> <args ordered="yes"> <Const type="&rif;iri">&ppl;John</Const> <Var>item</Var> </args> </Atom> </then> </Implies> </formula> </Forall> </sentence> <sentence> <Forall> <declare><Var>item</Var></declare> <formula> <Implies> <if> <Atom> <op><Const type="&rif;iri">&cpt;unsolicited</Const></op> <args ordered="yes"><Var>item</Var></args> </Atom> </if> <then> <Atom> <op><Const type="&rif;iri">&cpt;reject</Const></op> <args ordered="yes"> <Const type="&rif;iri">&ppl;Fred</Const> <Var>item</Var> </args> </Atom> </then> </Implies> </formula> </Forall> </sentence> </Group> </payload> </Document> 4.3 Mapping from the Presentation Syntax to the XML Syntax This section defines a normative mapping, core , from the presentation syntax to the XML syntax of RIF-Core. The mapping is given via tables where each row specifies the mapping of a particular syntactic pattern in the presentation syntax. These patterns appear in the first column of the tables and the bold-italic symbols represent metavariables. The second column represents the corresponding XML patterns, which may contain applications of the mapping core to these metavariables. When an expression core ( metavar ) occurs in an XML pattern in the right column of a translation table, it should be understood as a recursive application of core to the presentation syntax represented by the metavariable. The XML syntax result of such an application is substituted for the expression core ( metavar ) . A sequence of terms containing metavariables with subscripts is indicated by an ellipsis. A metavariable or a well-formed XML subelement is marked as optional by appending a bold-italic question mark, ? , on its right. 4.3.1 Mapping of the Condition Language The core mapping from the presentation syntax to the XML syntax of the RIF-Core Condition Language is specified by the table below. Each row indicates a translation core ( Presentation ) = XML . Since the presentation syntax of RIF-Core is context sensitive, the mapping must differentiate between the terms that occur in the position of the individuals and the terms that occur as atomic formulas. To this end, in the translation table, the positional and named argument terms that occur in the context of atomic formulas are denoted by the expressions of the form pred (...) and the terms that occur as individuals are denoted by expressions of the form func (...). In the table, each metavariable for an (unnamed) positional argument i is assumed to be instantiated to values unequal to the instantiations of named arguments unicodestring j -> filler j . Regarding the last but first row, we assume that shortcuts for constants [ RIF-DTB ] have already been expanded to their full form ( "..."^^ symspace ). Presentation Syntax XML Syntax And ( conjunct 1 . . . conjunct n ) <And> <formula> core ( conjunct 1 )</formula> . . . <formula> core ( conjunct n )</formula> </And> Or ( disjunct 1 . . . disjunct n ) <Or> <formula> core ( disjunct 1 )</formula> . . . <formula> core ( disjunct n )</formula> </Or> Exists variable 1 . . . variable n ( body ) <Exists> <declare> core ( variable 1 )</declare> . . . <declare> core ( variable n )</declare> <formula> core ( body )</formula> </Exists> External ( atomframexpr ) <External> <content> core ( atomframexpr )</content> </External> pred ( argument 1 . . . argument n ) <Atom> <op> core ( pred )</op> <args ordered="yes"> core ( argument 1 ) . . . core ( argument n ) </args> </Atom> pred ( unicodestring 1 -> filler 1 . . . unicodestring n -> filler n ) <Atom> <op> core ( pred )</op> <slot ordered="yes"> <Name> unicodestring 1 </Name> core ( filler 1 ) </slot> . . . <slot ordered="yes"> <Name> unicodestring n </Name> core ( filler n ) </slot> </Atom> inst [ key 1 -> filler 1 . . . key n -> filler n ] <Frame> <object> core ( inst )</object> <slot ordered="yes"> core ( key 1 ) core ( filler 1 ) </slot> . . . <slot ordered="yes"> core ( key n ) core ( filler n ) </slot> </Frame> inst # class <Member> <instance> core ( inst )</instance> <class> core ( class )</class> </Member> sub ## super <Subclass> _{core ( sub )} <super> core ( super )</super> </Subclass> " unicodestring "^^ symspace <Const type=" symspace "> unicodestring </Const> ? unicodestring <Var> unicodestring </Var> 4.3.2 Mapping of the Rule Language The core mapping from the presentation syntax to the XML syntax of the RIF-Core Rule Language is specified by the table below. It extends the translation table of Section Translation of RIF-Core Condition Language . While the Import directive is handled by the presentation-to-XML syntax mapping, the Prefix and Base directives are not. Instead, these directives should be handled by macro-expanding the associated shortcuts (compact URIs). Namely, a prefix name declared in a Prefix directive is expanded into the associated IRI, while relative IRIs are completed using the IRI declared in the Base directive. The mapping core applies only to such macro-expanded documents. RIF-Core also allows other treatments of Prefix and Base provided that they produce equivalent XML documents. One such treatment is employed in the examples in this document, especially Example 7. It replaces prefix names with definitions of XML entities as follows. Each Prefix declaration becomes an ENTITY declaration [ XML1.0 ] within a DOCTYPE DTD attached to the RIF-Core Document . The Base directive is mapped to the xml:base attribute [ XML-Base ] in the XML Document tag. Compact URIs of the form prefix:suffix are then mapped to &prefix;suffix . Presentation Syntax XML Syntax Document( Import( loc 1 prfl 1 ? ) . . . Import( loc n prfl n ? ) group ) <Document> <directive> <Import> <location> core ( loc 1 )</location> <profile> core ( prfl 1 )</profile> ? </Import> </directive> . . . <directive> <Import> <location> core ( loc n )</location> <profile> core ( prfl n )</profile> ? </Import> </directive> <payload> core ( group )</payload> </Document> Group( clause 1 . . . clause n ) <Group> <sentence> core ( clause 1 )</sentence> . . . <sentence> core ( clause n )</sentence> </Group> Forall variable 1 . . . variable n ( rule ) <Forall> <declare> core ( variable 1 )</declare> . . . <declare> core ( variable n )</declare> <formula> core ( rule )</formula> </Forall> conclusion :- condition <Implies> <if> core ( condition )</if> <then> core ( conclusion )</then> </Implies> 4.3.3 Mapping of Annotations The core mapping from RIF-Core annotations in the presentation syntax to the XML syntax is specified by the table below. It extends the translation tables of Sections Translation of RIF-Core Condition Language and Translation of RIF-Core Rule Language . The metavariable Typetag in the presentation and XML syntaxes stands for any of the class names And , Or , External , Document , or Group , and Quantifier for Exists or Forall . The dollar sign, $ , stands for any of the binary infix operator names # , ## , = , or :- , while Binop stands for their respective class names Member , Subclass , Equal , or Implies . Again, each metavariable for an (unnamed) positional argument i is assumed to be instantiated to values unequal to the instantiations of named arguments unicodestring j -> filler j . Presentation Syntax XML Syntax (* iriconst? frameconj? *) Typetag ( e 1 . . . e n ) < Typetag > <id> core ( iriconst )</id> ? <meta> core ( frameconj )</meta> ? e 1 ' . . . e n ' </ Typetag > where e 1 ' , . . ., e n ' are defined by the equation core ( Typetag ( e 1 . . . e n )) = < Typetag > e 1 ' . . . e n ' </ Typetag > (* iriconst? frameconj? *) Quantifier variable 1 . . . variable n ( body ) < Quantifier > <id> core ( iriconst )</id> ? <meta> core ( frameconj )</meta> ? <declare> core ( variable 1 )</declare> . . . <declare> core ( variable n )</declare> <formula> core ( body )</formula> </ Quantifier > (* iriconst? frameconj? *) pred ( argument 1 . . . argument n ) <Atom> <id> core ( iriconst )</id> ? <meta> core ( frameconj )</meta> ? <op> core ( pred )</op> <args ordered="yes"> core ( argument 1 ) . . . core ( argument n ) </args> </Atom> (* iriconst? frameconj? *) pred ( unicodestring 1 -> filler 1 . . . unicodestring n -> filler n ) <Atom> <id> core ( iriconst )</id> ? <meta> core ( frameconj )</meta> ? <op> core ( pred )</op> <slot ordered="yes"> <Name> unicodestring 1 </Name> core ( filler 1 ) </slot> . . . <slot ordered="yes"> <Name> unicodestring n </Name> core ( filler n ) </slot> </Atom> (* iriconst? frameconj? *) inst [ key 1 -> filler 1 . .it appears in at least one non-external, non-disjunctive atomic subformula of such that ?v is not in the scope of an existential quantifier within .

   key n -> filler n ] <Frame> <id> core ( iriconst )</id> ? <meta> core ( frameconj )</meta> ? <object> core ( inst )</object> <slot ordered="yes"> coreISSUES: The above is very unclear. What is a non-disjunctive atomic subformula?? ( key 1see above definition of a disjunctive subformula)  coreAn atomic formula is also non disjunctive. And it does not have quantifiers. What is  ( fillerfixed)?