W3C


RIF Basic Logic Dialect

W3C Editor's Draft 0710 April 2008

This version:
http://www.w3.org/2005/rules/wg/draft/ED-rif-bld-20080407/http://www.w3.org/2005/rules/wg/draft/ED-rif-bld-20080410/
Latest editor's draft:
http://www.w3.org/2005/rules/wg/draft/rif-bld/
Previous version:
http://www.w3.org/2005/rules/wg/draft/ED-rif-bld-20080222/http://www.w3.org/2005/rules/wg/draft/ED-rif-bld-20080407/ (color-coded diff)
Editors:
Harold Boley, National Research Council Canada
Michael Kifer, State University of New York at Stony Brook


Abstract

This document, developed by the Rule Interchange Format (RIF) Working Group, specifies a basic format that allows logic rules to be exchanged between rule-based systems.

A separate document RIF Data Types and Built-Ins describes data types and built-in functions and predicates.

Status of this Document

May Be Superseded

This section describes the status of this document at the time of its publication. Other documents may supersede this document. A list of current W3C publications and the latest revision of this technical report can be found in the W3C technical reports index at http://www.w3.org/TR/.

This document is being published as one of a set of 23 documents:

  1. RIF Basic Logic Dialect (this document)
  2. RIF Framework for Logic Dialects
  3. RIF RDF and OWL Compatibility

Note for Working Group

This draft is ready for Working Group Review. A publication decision is scheduled for 15 April.

Please Comment By 2008-04-082008-04-14

The Rule Interchange Format (RIF) Working Group seeks public feedback on these Working Drafts. Please send your comments to public-rif-comments@w3.org (public archive). If possible, please offer specific changes to the text that would address your concern. You may also wish to check the Wiki Version of this document for internal-review comments and changes being drafted which may address your concerns.

No Endorsement

Publication as a Working Draft does not imply endorsement by the W3C Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress.

Patents

This document was produced by a group operating under the 5 February 2004 W3C Patent Policy. W3C maintains a public list of any patent disclosures made in connection with the deliverables of the group; that page also includes instructions for disclosing a patent. An individual who has actual knowledge of a patent which the individual believes contains Essential Claim(s) must disclose the information in accordance with section 6 of the W3C Patent Policy.


Contents

1 Overview

This document develops RIF-BLD (the Basic Logic Dialect of the Rule Interchange F ormat) based on a set of foundational concepts that are supposed to be shared by all logic-based RIF dialects.ormat). From a theoretical perspective, RIF-BLD corresponds to the language of definite Horn rules (see Horn Logic) with equality and with a standard first-order semantics. Syntactically, RIF-BLD has a number of extensions to support features such as objects and frames a as in F-logic [KLW95], internationalized resource identifiers (or IRIs, defined by RFC 3987[RFC-3987]) as identifiers for concepts, and XML Schema data types. In addition, the document RIF RDF and OWL Compatibility defines the syntax and semantics of integrated RIF-BLD/RDF and RIF-BLD/OWL languages. These features make RIF-BLD intoa Web language .Web-aware language. However, it should be kept in mind that RIF is designed to enable interoperability among rule languages in general, and its uses are not limited to the Web.

One important fragment of RIF is called the Condition Language. It defines the syntax and semantics for the bodiesif-parts of the rules in RIF-BLD. However, it is envisioned that this fragment will have uses in other dialects of RIF. In particular, it willcan be used as queries, constraints, and in the conditional part inof production rules (see RIF-PRD ), reactive rules,) and normativereactive rules.

RIF-BLD is defined in two different ways -- both normative . First, it is defined:

  • As a specialization of the RIF Framework for Logic-based Dialects (RIF-FLD) --, which is part of the RIF extensibility framework.

    ItThis version of the RIF-BLD specification is avery short description, but it requires familiarity with RIF-FLD. RIF-FLD provides a general framework -- both syntacticand semantic -- for defining RIF dialects. All logic-based dialects are required to specializeis presented at the end of this framework. Thendocument, in Section RIF-BLD is described independentlyas a Specialization of the RIF framework,Framework. It is intended for the benefit of thosereader who desire a quicker path to RIF-BLD and areis familiar with RIF-FLD and, therefore, does not interested in the extensibility issues.need to go through the currentmuch longer direct specification of RIF-BLD. This version of the specification is also useful for dialect designers, as it is a concrete example of how a non-trivial RIF dialect can be derived from the RIF framework.

  • Independently of the RIF framework, for the benefit of those who desire a quicker path to RIF-BLD and are not interested in the extensibility issues. This version of the RIF-BLD specification is given first.

The current document is the thirdlatest draft of the RIF-BLD specification. A number of extensions are planned to support built-ins, additional primitive XML data types, the notion of RIF compliance, and so on. Tool support for RIF-BLD is forthcoming. RIF dialects that extend RIF-BLD in accordance with the RIF Framework for Logic Dialects will be specified in other documents by this working group.


2 RIF-BLD as a SpecializationDirect Specification of the RIF FrameworkRIF-BLD Syntax

This normative section describesspecifies the syntax of RIF-BLD by specializing RIF-FLD.directly, without relying on RIF-FLD. We define both a presentation syntax and an XML syntax. The readerpresentation syntax is assumednot intended to be familiar with RIF-FLD as described in RIF Frameworka concrete syntax for Logic-Based Dialects . The reader whoRIF-BLD. It is not interesteddefined in how RIF-BLD is derived from the framework can skip this sectionMathematical English and proceedis intended to Direct Specification of RIF-BLD Syntax . 2.1be used in the definitions and examples. This syntax of RIF-BLDdeliberately leaves out details such as a Specialization of RIF-FLD This section defines the precise relationship betweenthe syntaxdelimiters of RIF-BLD andthe various syntactic framework of RIF-FLD. The syntaxcomponents, escape symbols, parenthesizing, precedence of operators, and the like. Since RIF Basic Logic Dialectis defined by specialization from the syntaxan interchange format, it uses XML as its concrete syntax.

2.1 Alphabet of the RIF Syntactic Framework for Logic DialectsRIF-BLD

Definition (Alphabet). Section SyntaxThe alphabet of RIF-BLD consists of

  • a RIF Dialect ascountably infinite set of constant symbols Const
  • a Specializationcountably infinite set of the RIF Framework in that document lists the parametersvariable symbols Var (disjoint from Const)
  • a countably infinite set of argument names, ArgNames (disjoint from Const and Var)
  • connective symbols And, Or, and :-
  • quantifiers Exists and Forall
  • the syntactic framework, which we will now specialize for RIF-BLD. Alphabet .symbols =, #, ##, ->, and External
  • the alphabetgrouping symbol Group
  • auxiliary symbols, such as "(" and ")"

The set of RIF-BLDconnective symbols, quantifiers, =, etc., is disjoint from Const and Var. The alphabet of RIF-FLDargument names in ArgNames are written as unicode strings that must not start with a question mark, "?". Variables are written as Unicode strings preceded with the negation symbols Neg and Naf excluded. Assignmentsymbol "?".

Constants are written as "literal"^^symspace, where literal is a sequence of signatures to each constantUnicode characters and symspace is an identifier for a symbol space. Symbol spaces are defined in Section Symbol Spaces of the RIF-FLD document.

The signature setdefinition of RIF-BLD containssymbol spaces will eventually be also given in the following signatures: Basic. individual{ } atomic{ }document Data Types and Builtins, so the signature individual{ } representsabove reference will be to that document instead of RIF-FLD.

The contextsymbols =, #, and ## are used in which individual objects (but not atomic formulas) can appear.formulas that define equality, class membership, and subclass relationships. The signature atomic{ } representssymbol -> is used in terms that have named arguments and in frame formulas. The context wheresymbol External indicates that an atomic formulas can occur. For every integer n 0 , there are signatures f n {(individual ... individual) individual} -- for n-ary function symbols, p n {(individual ... individual) atomic} -- for n-ary predicates. These representformula or a function term is defined externally (e.g., a builtin).

The symbol Group is used to organize RIF-BLD rules into collections and predicate symbolsannotate them with metadata.   ☐

The language of arity n (eachRIF-BLD is the set of formulas constructed using the above cases has n individual s as arguments insidealphabet according to the parentheses). For every setrules given below.


2.2 Terms

RIF-BLD supports several kinds of symbols s1 ,..., sk SigNames , there are signatures f s1...sk {(s1->individual ... sk->individual) individual}terms: constants and p s1...sk {(s1->individual ... sk->individual) atomic} . These are signatures forvariables, positional terms, terms with named arguments and predicates with arguments named s1, ..., skequality, respectively. Unlike in RIF-FLD, the argument names s1membership, ..., sk mustand subclass atomic formulas, and frame formulas. The word "term" will be pairwise distinct.used to refer to any kind of these constructs.

Definition (Term).

  1. Constants and variables. If t Const or t Var then t is a symbol insimple term.
  2. Positional terms. If t Const can have exactly one signature, individual , f nand t1, or p..., tn are simple, where n 0positional, or f s1...sk {(s1->individual ... sk->individual) individual} , p s1...sk {(s1->individualnamed-argument terms then t(t1 ... sk->individual) atomic} , for some s1 ,..., sk SigNames . It cannot have the signature atomic , since only complex terms can have such signatures. Thus, by itself a symbol cannot be a proposition in RIF-BLD, buttn) is a positional term of the form p() can be. Thus, in RIF-BLD each constant symbol can be either an individual,.
  3. Terms with named arguments. A predicate of one particular arity orterm with certain argument names, an externally defined predicate of one particular arity, or an externally defined function symbol of one particular arity -- itnamed arguments is not possible for the same symbol to play more than one role. The constant symbols that belong toof the supported RIF data types (XML Schema data types, rdf:XMLLiteral , rif:textform t(s1->v1 ... sn->vn) all have the signature individual in RIF-BLD. The symbols of type rif:iri, where t Const and rif:local can have the following signatures in RIF-BLD: individualv1, f..., vn are simple, positional, or p nnamed-argument terms and s1, for..., sn = 0,1,.... ;are pairwise distinct symbols from the set ArgNames.

    The term t here represents a predicate or f s1...ska function; s1, p s1...sk..., sn represent argument names; and v1, for some..., vn represent argument names s1 ,..., sk SigNames . All variablesvalues. The argument names, s1, ..., sn, are associatedrequired to be pairwise distinct. Terms with signature individual{ } , so they can range only over individuals. The signature for equality is ={(individual individual) atomic} . This means that equality can compare only those terms whose signature is individual ; it cannot compare predicate names or function symbols. Equality termsnamed arguments are also not allowed to occur inside other terms, sincelike positional terms except that the above signature impliesarguments are named and their order is immaterial. Note that anya term of the form t = s has signature atomicf() is both positional and not individualwith named arguments.

  4. Equality terms. The frame signature, ->If t and s are simple, positional, or named-argument terms then t = s is ->{(individual individual individual) atomic} . Note that this precludes the possibility that a frame term might occur asan argument to a predicate, a function, or inside some other term. Theequality term.
  5. Class membership signature, # ,terms (or just membership terms). t#s is #{(individual individual) atomic} . Note that this precludes the possibility thata membership term might occur as an argument to a predicate, a function,if t and s are simple, positional, or inside some other term. The signature for thenamed-argument terms.
  6. Subclass relationship is ##{(individual individual) atomic}terms. As with frames and membership terms, this precludes the possibility thatt##s is a subclass term might occur inside some other term. RIF-BLD uses no special syntax for declaring signatures. Instead, the author specifies signatures contextuallyif t and s are simple, positional, or named-argument terms.
  7. Frame terms. That is, since RIF-BLD requires that each symbolt[p1->v1 ... pn->vn] is associated witha unique signature, the signature is determined from the context in which the symbol is used.frame term (or simply a frame) if t, p1, ..., pn, v1, ..., vn, n 0, are simple, positional, or named-argument terms.
  8. Externally defined terms. If t is a symbolterm then External(t) is an externally defined term.
  9. Such terms are used in more than one context, the parser must treat thisfor representing builtin functions and predicates as a syntax error. If no errors are found, allwell as "procedurally attached" terms and atomic formulas are guaranteed to be well-formed. Thus, signaturesor predicates, which might exist in various rule-based systems, but are not part of the RIF-BLD language, and individualspecified by RIF.   ☐

Membership, subclass, and atomicframe terms are not reserved keywords in RIF-BLD. Supported typesused to describe objects and class hierarchies.


2.3 Well-formedness of Terms

. RIF-BLD supports all the term types defined byThe syntactic framework (see Well-formed Terms and Formulas ): constants variablesset of all symbols, Const, is partitioned into

  • positional predicate symbols
  • predicate symbols with named arguments
  • equality frame membership subclass external Compared to RIF-FLD, terms (bothpositional andfunction symbols
  • function symbols with named arguments) have significant restrictions. This is soarguments
  • individuals.

    The symbols in orderConst that belong to give BLD a relatively compact nature.the signaturesupported RIF data types are individuals.

Each predicate and function symbol has precisely one arity.

  • For positional symbols, an arity is a non-negative integer that tells how many arguments the variablesymbol can take.
  • For symbols does not permit them to occur in the context of predicates, functions, or formulas. In particular, unlike in RIF-FLD, a variable is notthat take named arguments, an atomic formula in RIF-BLD. Likewise,arity is a symbol cannot be an atomic formula by itself. That is, if pset {s1 ... sk} of argument names (si Const then pArgNames), which are allowed for that symbol.

The arity of a symbol (or whether it is nota well-formed atomic formula. However, p() can bepredicate, a function, or an atomic formula. Signatures permit onlyindividual) is not specified in RIF-BLD explicitly. Instead, it is inferred as follows. Each constant symbols to occursymbol in the contexta RIF-BLD formula (or a set of formulas) may occur in at most one context: as an individual, a function symbol of a particular arity, or a predicate names. Indeed, RIF-BLD signatures ensure that all variables have the signature individual{ } and all other terms, except forsymbol of a particular arity. The constants from Const , can have eitherarity of the signature individual{ } or atomic{ } . Therefore, if tsymbol and its type is then determined by its context. If a (non-symbol from Const ) term then t(...)occurs in more than one context in a set of formulas, the set is not awell-formed term. Supported symbol spaces . RIF-BLD supports allin RIF-BLD.

For a term of the symbol spacesform External(t) to be well-formed, t must be an instance of an external schema, i.e., a schema of an externally specified term, as defined in Section Symbol SpacesSchemas for Externally Defined Terms of RIF-FLD.

Also, if a term of the syntactic framework: xsd:string xsd:decimal xsd:time xsd:date xsd:dateTime rdf:XMLLiteral rif:text rif:iri rif:local Supported formulas . RIF-BLD supportsform External(p(...)) occurs as an atomic formula then the following typesoccurrence of formulas (see Well-formed Terms and Formulas for the definitions): RIF-BLD condition A RIF-BLD conditionp is considered to be a conjunctivepredicate occurrence.


The definition of external schemas will eventually also appear in the document Data Types and disjunctive combinationBuiltins, so the above reference will be to that document instead of atomicRIF-FLD.


2.4 Formulas

Any term (positional or with optional existential quantificationnamed arguments) of variables. RIF-BLD rulethe form p(...) (or External(p(...)), where p is a RIF-BLD rulepredicate symbol, is also an atomic formula. Equality, membership, subclass, and frame terms are also atomic formulas. A universally quantified RIF-FLD rule with the following restrictions: The head (or conclusion)formula of the ruleform External(p(...)) is also called an externally defined atomic formula, which isformula.

Simple terms (constants and variables) are not formulas. Not all atomic formulas are well-formed. A well-formed atomic formula is an externally defined predicate (i.e., it cannot have the form External(...) ). The body (or premise) of the ruleatomic formula that is also a RIF-BLD condition. All free (non-quantified) variables inwell-formed term (see Section Well-formedness of Terms). More general formulas are constructed out of the rule must be quantifiedatomic formulas with Forall outside ofthe rule (i.e., Forall ?vars (head :- body) ). RIF-BLD grouphelp of logical connectives.

Definition (Well-formed formula). A RIF-BLD groupwell-formed formula is a RIF-FLD group that contains only RIF-BLD rules and RIF-BLD groups. Recallstatement that negation (classical or default) is not supported by RIF-BLD in either the rule head or the body.has one of the list of supported symbol spaces will move to another document, Data Typesfollowing forms:

  • Atomic: If φ is a well-formed atomic formula then it is also a well-formed formula.
  • Conjunction: If φ1, ..., φn, n 0, are well-formed formulas then so is And(φ1 ... φn), called a conjunctive formula. As a special case, And() is allowed and Built-Ins . Any existing discrepancies will be fixed atis treated as a tautology, i.e., a formula that time. 2.2 The Semantics of RIF-BLDis always true.
  • Disjunction: If φ1, ..., φn, n 0, are well-formed formulas then so is Or(φ1 ... φn), called a disjunctive formula. When n=0, we get Or() as a Specialization of RIF-FLD This normative section defines the precise relationship between the semantics of RIF-BLDspecial case; it is treated as a contradiction, i.e., a formula that is always false.
  • Existentials: If φ is a well-formed formula and the semantic framework of RIF-FLD. Specification of the semantics without reference to RIF-FLD?V1, ..., ?Vn are variables then Exists ?V1 ... ?Vn(φ) is given in Section Direct Specification ofan existential formula.

Formulas constructed using the above definitions are called RIF-BLD Semanticsconditions. The semantics of the RIF Basic Logic Dialect is defined by specialization from the semantics offollowing formulas lead to the Semantic Framework for Logic Dialects of RIF. Section Semanticsnotion of a RIF Dialect as a Specialization of the RIF Framework in that document lists the parameters of the semantic framework, which we need to specialize for RIF-BLD. Recall that the semantics of a dialectRIF-BLD rule.

  • Rule implication: If φ is derived from these notions by specializing the following parameters. The effect of the syntax .an well-formed atomic formula and ψ is a RIF-BLD condition then φ :- ψ is a well-formed formula, called rule implication, provided that φ is not externally defined (i.e., does not support negation. This is the only obvious simplification with respect to RIF-FLD as far ashave the semanticsform External(...)).
  • Quantified rule: If φ is concerned. Truth values . The set TV of truth values in RIF-BLD consists of just two values, ta rule implication and f such that f < t t . Clearly, < t?V1, ..., ?Vn are variables then Forall ?V1 ... ?Vn(φ) is a total order here. Data typeswell-formed formula, called quantified rule. RIF-BLD supportsIt is required that all the data types listed in Section Primitive Data Types of RIF-FLD: xsd:long xsd:integer xsd:decimal xsd:string xsd:time xsd:dateTime rdf:XMLLiteral rif:text Logical entailment . Recall that logical entailmentfree (i.e., non-quantified) variables in RIF-FLD is defined with respect to an unspecified set of intended semantic structures and that dialects of RIF must make this notion concrete. For RIF-BLD, this set is definedφ occur in one ofthe two following equivalent ways: as a set of all models; orprefix Forall ?V1 ... ?Vn. Quantified rules will also be referred to as the unique minimal model. These two definitions are equivalent for entailment ofRIF-BLD conditions byrules.
  • Group: If φ is a frame term and ρ1, ..., ρn are RIF-BLD rules or group formulas (they can be mixed) then Group φ 1 ... ρn) and Group 1 ... ρn) are group formulas.

    Group formulas are intended to represent sets of formulas, since allrules in RIF-BLD are Horn -- itannotated with metadata. This metadata is a classical resultspecified using an optional frame term φ. Note that some of Van Emden and Kowalski [ vEK76 ].the list of supported data types will move to another document, Data Types and Built-Ins . Any existing discrepancies willρi's can be fixed atgroup formulas themselves, which means that time. 3 Direct Specification of RIF-BLD Syntaxgroups can be nested. This normative section specifies the syntax of RIF-BLD directly, without referringallows one to RIF-FLD. We define both a presentation syntax and an XML syntax. The presentation syntax is not intendedattach metadata to various subsets of rules, which may be a concrete syntax for RIF-BLD. It is definedinside larger rule sets, which in Mathematical English and is intended toturn can be used inannotated.   ☐


It can be seen from the definitions that RIF-BLD has a wide variety of syntactic forms for terms and examples.formulas. This syntax deliberately leaves out details such asprovides the delimitersinfrastructure for exchanging rule languages that support rich collections of the varioussyntactic components, escape symbols, parenthesizing, precedenceforms. Systems that do not support some of operators, and the like. Since RIF is an interchange format, it uses XML as its concrete syntax. 3.1 Alphabetthat syntax directly can still support it through syntactic transformations. For instance, disjunctions in the rule body can be eliminated through a standard transformation, such as replacing p :- Or(q r) with a pair of RIF-BLD Definition (Alphabet)rules p :- q,   p :- r. Terms with named arguments can be reduced to positional terms by ordering the alphabetarguments by their names and incorporating them into the predicate name. For instance, p(bb->1 aa->2) can be represented as p_aa_bb(2,1).


2.5 EBNF Grammar for the Presentation Syntax of RIF-BLD

consistsSo far, the syntax of RIF-BLD has been specified in Mathematical English. Tool developers, however, may prefer EBNF notation, which provides a countably infinite setmore succinct overview of constant symbols Const a countably infinite setthe syntax. Several points should be kept in mind regarding this notation.

  • The syntax of variable symbols Var (disjoint from Const ) a countably infinite setfirst-order logic is not context-free, so EBNF does not capture the syntax of argument names, ArgNames (disjoint from Const and Var ) connective symbols And , Or , and :- quantifiers Exists and ForallRIF-BLD precisely. For instance, it cannot capture the symbols = , # , ## , ->section on well-formedness conditions, and Externali.e., the groupingrequirement that each symbol Group auxiliary symbols, suchin RIF-BLD can occur in at most one context. As "(" and ")"a result, the setEBNF grammar defines a strict superset of connective symbols, quantifiers, = , etc., is disjoint from Const and Var . The argument names in ArgNamesRIF-BLD (not all rules that are written as unicode strings that mustderivable using the EBNF grammar are well-formed rules in RIF-BLD).
  • The EBNF syntax is not start witha question mark, " ? ". Variables are written as Unicode strings preceded withconcrete syntax: it does not address the symbol " ? ".details of how constants and variables are writtenrepresented, and it is not sufficiently precise about the delimiters and escape symbols. Instead, white space is informally used as "literal"^^symspacea delimiter, and white space is implied in productions that use Kleene star. For instance, TERM* is to be understood as TERM TERM ... TERM, where literaleach ' ' abstracts from one or more blanks, tabs, newlines, etc. This is done on intentionally, since RIF's presentation syntax is intended as a sequence of Unicode characterstool for specifying the semantics and symspacefor illustration of the main RIF concepts through examples. It is an identifiernot intended as a concrete syntax for a symbol space. Symbol spaces are defined in Section Symbol Spacesrule language. RIF defines a concrete syntax only for exchanging rules, and that syntax is XML-based, obtained as a refinement and serialization of the RIF-FLD document .EBNF syntax.
  • For all the definition of symbol spaces will eventually be also given inabove reasons, the document Data Types and Builtins , soEBNF syntax is not normative.

2.5.1 EBNF for the above reference will be to that document instead of RIF-FLD.RIF-BLD Condition Language

The symbols = , # , and ## are used inCondition Language represents formulas that define equality, class membership, and subclass relationships. The symbol -> iscan be used in terms that have named arguments and in frame formulas.the symbol External indicates that an atomic formula or a function term is defined externally (e.g., a builtin).body of the symbol GroupRIF-BLD rules. It is usedintended to organize RIF-BLD rules into collections and annotate them with metadata.   ☐be a common part of a number of RIF dialects, including RIF PRD. The languageEBNF grammar for a superset of the RIF-BLD condition language is as follows.


  FORMULA        ::= 'And' '(' FORMULA* ')' |
                     'Or' '(' FORMULA* ')' |
                     'Exists' Var+ '(' FORMULA ')' |
                     ATOMIC |
                     'External' '(' Atom ')'
  ATOMIC         ::= Atom | Equal | Member | Subclass | Frame
  Atom           ::= UNITERM
  UNITERM        ::= Const '(' (TERM* | (Name '->' TERM)*) ')'
  Equal          ::= TERM '=' TERM
  Member         ::= TERM '#' TERM
  Subclass       ::= TERM '##' TERM
  Frame          ::= TERM '[' (TERM '->' TERM)* ']'
  TERM           ::= Const | Var | Expr | 'External' '(' Expr ')'
  Expr           ::= UNITERM
  Const          ::= '"' UNICODESTRING '"^^' SYMSPACE
  Name           ::= UNICODESTRING
  Var            ::= '?' UNICODESTRING


The set of formulas constructed usingproduction rule for the above alphabet according tonon-terminal FORMULA represents RIF condition formulas (defined earlier). The rules given below. 3.2 Terms RIF-BLD supports several kinds of terms: constantsconnectives And variables , positional terms, terms with named arguments , equality , membership ,and subclass atomic formulas,Or define conjunctions and frame formulas.disjunctions of conditions, respectively. Exists introduces existentially quantified variables. Here Var+ stands for the word " term " will be used to refer to any kindlist of these constructs. Definition (Term) . Constants andvariables that are free in FORMULA. If t Const or t Var then t isRIF-BLD conditions permit only existential variables, but RIF-FLD Syntax allows arbitrary quantification, which can be used in some dialects. A simple term . Positional terms . If t Const and t 1RIF-BLD FORMULA can also be an ATOMIC term, i.e. an Atom, ..., t n are simpleExternal Atom, positionalEqual, Member, Subclass, or named-argument terms then t(t 1 ... t n ) is a positional term . Terms with named argumentsFrame. A TERM with named arguments is of the form t(s 1 ->v 1 ... s n ->v n ) , where t Const and v 1 , ..., v n are simple , positionalcan be a constant, variable, Expr, or named-argument terms and s 1 , ..., s n are pairwise distinct symbols from the set ArgNamesExternal Expr.

The term t here represents a predicate or a function; s 1 , ..., s n represent argument names;RIF-BLD presentation syntax does not commit to any particular vocabulary except for using Unicode strings in constant symbols, as names, and v 1 , ..., v n represent argument values.for variables. Constant symbols have the argument names, s 1 , ..., s nform: "UNICODESTRING"^^SYMSPACE, are required to be pairwise distinct. Terms with named arguments are like positional terms exceptwhere SYMSPACE is an IRI string that identifies the arguments are namedsymbol space of the constant and their orderUNICODESTRING is immaterial. Note thata term ofUnicode string from the form f() is both positional and with named arguments. Equality terms . If t and slexical space of that symbol space. Names are simple , positional , or named-argument terms then t = s is an equality term . Class membership terms (orjust membership terms ). t#s is a membership term if t and sdenoted by Unicode character sequences. Variables are simple , positional , or named-argument terms.denoted by Unicode character sequences beginning with a ?-sign. Equality, membership, and subclass terms . t##s is a subclass term if t and sare simple ,self-explanatory. An Atom and Expr (expression) can either be positional ,or named-argument terms.with named arguments. A frame terms . t[p 1 ->v 1 ... p n ->v n ]term is a frameterm (or simplycomposed of an object Id and a frame ) if t , p 1 , ..., p n , v 1 , ..., v n , n 0 , are simple , positional , or named-argument terms.collection of attribute-value pairs. An External Atom is a call to an externally defined terms. If tpredicate of RIF-DTB. Likewise, an External Expr is a term then External(t) iscall to an externally defined termfunction of RIF-DTB.


Such termsExample 1 (RIF-BLD conditions).

This example shows conditions that are used for representing builtin functionscomposed of atoms, expressions, frames, and predicates as well as "procedurally attached" terms or predicates, which might existexistentials. In various rule-based systems, but are not specified by RIF.   ☐ Membership, subclass, andframe termsformulas variables are used to describe objects and class hierarchies. 3.3 Well-formedness of Termsshown in the setpositions of all symbols, Const , is partitioned into positional predicate symbols predicate symbols with named arguments positional function symbols function symbols with named arguments individuals. The symbols in Const that belong to the supported RIF data types are individuals. Each predicate and function symbol has precisely one arity .object Ids, object properties, or property values. For positional symbols, an arity is a non-negative integer that tells how many argumentsbrevity, we use the symbol can take. For symbols that take named arguments, an arity is a set {s 1 ... s k } of argument names ( s i ArgNames ),compact URI notation [CURIE], prefix:suffix, which are allowed for that symbol. The arity of a symbol (or whether it is a predicate, a function, or an individual) is not specified in RIF-BLD explicitly. Instead, it is inferred as follows. Each constant symbol in a RIF-BLD formula (or a set of formulas) may occur in at most one context:should be understood as an individual, a function symbol of a particular arity, ora predicate symbol ofmacro that expands into a particular arity. The arityconcatenation of the symbolprefix definition and its type is then determined by its context.suffix. Thus, if bks is a symbol from Const occurs in more than one context in a set of formulas,prefix that expands into http://example.com/books# then bks:LeRif should be understood merely as an abbreviation for http://example.com/books#LeRif. The setcompact URI notation is not well-formed in RIF-BLD. For a termpart of the form External(t) to be well-formed, t must be an instance of an external schema , i.e., a schema of an externally specified term, as defined in Section Schemas for Externally DefinedRIF-BLD syntax.


Compact URI prefixes:

  bks  expands into http://example.com/books#
  auth expands into http://example.com/authors#
  cpt  expands into http://example.com/concepts#
Positional terms:

  "cpt:book"^^rif:iri("auth:rifwg"^^rif:iri "bks:LeRif"^^rif:iri)
  Exists ?X ("cpt:book"^^rif:iri(?X "bks:LeRif"^^rif:iri))

Terms  of RIF-FLD. Also, if a term ofwith named arguments:

  "cpt:book"^^rif:iri(cpt:author->"auth:rifwg"^^rif:iri
                      cpt:title->"bks:LeRif"^^rif:iri)
  Exists ?X ("cpt:book"^^rif:iri(cpt:author->?X cpt:title->"bks:LeRif"^^rif:iri))

Frames:

  "bks:wd1"^^rif:iri["cpt:author"^^rif:iri->"auth:rifwg"^^rif:iri
                     "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]
  Exists ?X ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->?X
                                "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri])
  Exists ?X ("bks:wd2"^^rif:iri # "cpt:book"^^rif:iri["cpt:author"^^rif:iri->?X
                                                      "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri])
  Exists ?I ?X (?I["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri])
  Exists ?I ?X (?I # "cpt:book"^^rif:iri["cpt:author"^^rif:iri->?X
                                         "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri])
  Exists ?S ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->"auth:rifwg"^^rif:iri
                                ?S->"bks:LeRif"^^rif:iri])
  Exists ?X ?S ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->?X
                                   ?S->"bks:LeRif"^^rif:iri])
  Exists ?I ?X ?S (?I # "cpt:book"^^rif:iri[author->?X ?S->"bks:LeRif"^^rif:iri])


2.5.2 EBNF for the form External(p(...)) occurs as an atomic formula thenRIF-BLD Rule Language

The occurrence of p is considered to be a predicate occurrence.presentation syntax for Horn rules extends the definition of external schemas will eventually also appearsyntax in the document Data Types and Builtins , so the above reference will be to that document instead of RIF-FLD. 3.4 Formulas Any term (positional orSection EBNF for RIF-BLD Condition Language with named arguments) ofthe form p(...) (or External(p(...)) , where p is a predicate symbol, is also an atomic formula . Equality, membership, subclass, andfollowing productions.


  Group    ::= 'Group' IRIMETA? '(' (RULE | Group)* ')'
  IRIMETA  ::= Frame
   terms are alsoRULE     ::= 'Forall' Var+ '(' CLAUSE ')' | CLAUSE
  CLAUSE   ::= Implies | ATOMIC
   formulas. AImplies  ::= ATOMIC ':-' FORMULA

For convenient reference, we reproduce the condition language part of the form External(p(...)) is also called an externally defined atomic formula. Simple terms (constants and variables) are not formulas. Not all atomic formulas are well-formed. A well-formed atomicEBNF below.

  FORMULA         is an atomic::= 'And' '(' FORMULA* ')' |
                     'Or' '(' FORMULA* ')' |
                     'Exists' Var+ '(' FORMULA  that')' |
                     ATOMIC |
                     'External' '(' Atom ')'
  ATOMIC         ::= Atom | Equal | Member | Subclass | Frame
  Atom           ::= UNITERM
  UNITERM        ::= Const '(' (TERM* | (Name '->' TERM)*) ')'
  Equal          ::= TERM '=' TERM
  Member         ::= TERM '#' TERM
  Subclass       ::= TERM '##' TERM
  Frame          ::= TERM '[' (TERM '->' TERM)* ']'
  TERM           ::= Const | Var | Expr | 'External' '(' Expr ')'
  Expr           ::= UNITERM
  Const          ::= '"' UNICODESTRING '"^^' SYMSPACE
  Name           ::= UNICODESTRING
  Var            ::= '?' UNICODESTRING


A RIF-BLD Group is alsoa well-formed term (see Section Well-formednessnested collection of Terms ). More general formulas are constructed outRIF-BLD rules annotated with optional metadata, IRIMETA, represented as Frames. A Group can contain any number of the atomic formulasRULEs along with any number of nested Groups. Rules are generated by CLAUSE, which can be in the helpscope of logical connectives. Definition (Well-formed formula) .a well-formed formula isForall quantifier. If a statement thatCLAUSE in the RULE production has onea free (non-quantified) variable, it must occur in the Var+ sequence. Frame, Var, ATOMIC, and FORMULA were defined as part of the following forms:syntax for positive conditions in Section EBNF for RIF-BLD Condition Language. In the CLAUSE production an ATOMIC : If φis treated as a well-formed atomic formula thenrule with an empty condition part -- in which case it is alsousually called a well-formed formula. Conjunction : If φ 1 , ..., φ n , n 0 , are well-formed formulas then so is And(φ 1 ... φ n ) , called a conjunctive formula. As a special case, And() is allowed and is treated as a tautology, i.e.,fact. Note that, by a formula that is always true. Disjunction : If φ 1 , ..., φ n , n 0 , are well-formeddefinition in Section Formulas then so is Or(φ 1 ... φ n ) , called a disjunctive formula. When n=0, we get Or() as a special case; it is treated as a contradiction, i.e., a formulaformulas that is always false. Existentials : If φ is a well-formed formula and ?V 1 , ..., ?V n are variables then Exists ?V 1 ... ?V n (φ) is an existential formula.query externally defined atoms (i.e., formulas constructed usingof the above definitionsform External(Atom(...))) are called RIF-BLD conditions . The following formulas lead tonot allowed in the notionconclusion part of a RIF-BLD rule.rule implication : If φ is an well-formed(ATOMIC formula and ψ is a RIF-BLD condition then φ :- ψ is a well-formed formula, called rule implication , provided that φ is not externally defined (i.e.,does not have the form External(...)expand to External).


QuantifiedExample 2 (RIF-BLD rules).

This example shows a business rule borrowed from the document RIF Use Cases and Requirements:

If φan item is a rule implicationperishable and ?V 1 , ..., ?V n are variables then Forall ?V 1 ... ?V n (φ) is a well-formed formula, called quantified rule .it is required that all the free (i.e., non-quantified) variables in φ occur indelivered to John more than 10 days after the prefix Forall ?V 1 ... ?V n . Quantified rulesscheduled delivery date then the item will alsobe referred torejected by him.

As RIF-BLD rules . Group : If φ is a frame term and ρ 1 , ..., ρ n are RIF-BLD rules or group formulas (they can be mixed) then Group φ 1 ... ρ nbefore, for better readability we use the compact URI notation.

Compact URI prefixes:

  ppl expands into http://example.com/people#
  cpt expands into http://example.com/concepts#
  op  expands into the yet-to-be-determined IRI for RIF builtin predicates
a. Universal form:

   Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays (
        "cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item) :-
            And("cpt:perishable"^^rif:iri(?item)
                "cpt:delivered"^^rif:iri(?item ?deliverydate "ppl:John"^^rif:iri)
                "cpt:scheduled"^^rif:iri(?item ?scheduledate)
                External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration))
                External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffduration ?diffdays))
                External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))
   )

 and Group  1 ... ρ nb. Universal-existential form:

   Forall ?item (
        "cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item )  are group formulas .:-
            Exists ?deliverydate ?scheduledate ?diffduration ?diffdays (
                 And("cpt:perishable"^^rif:iri(?item)
                     "cpt:delivered"^^rif:iri(?item ?deliverydate "ppl:John"^^rif:iri)
                     "cpt:scheduled"^^rif:iri(?item ?scheduledate)
                     External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration))
                     External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffduration ?diffdays))
                     External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))
            )
   )



Example 3 (A RIF-BLD group formulas are intended to represent sets of rulesannotated with metadata.metadata).

This metadata is specified using an optional frame term φ . Noteexample shows a group formula that someconsists of two RIF-BLD rules. The ρ i 's can be group formulas themselves, which means that groups can be nested. This allows one to attach metadata to various subsetsfirst of rules, which may be inside larger rule sets, which in turn can be annotated.   ☐ It can be seenthese rules is copied from Example 2a. The definitions that RIF-BLD has a wide varietygroup is annotated with Dublin Core metadata represented as a frame.

Compact URI prefixes:

  bks  expands into http://example.com/books#
  auth expands into http://example.com/authors#
  cpt  expands into http://example.com/concepts#
  dc   expands into http://dublincore.org/documents/dces/
  w3   expands into http://www.w3.org/
Group "http://sample.org"^^rif:iri["dc:publisher"^^rif:iri->"w3:W3C"^^rif:iri
                                   "dc:date"^^rif:iri->"2008-04-04"^^xsd:date]
  (

    Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays (
        "cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item) :-
            And("cpt:perishable"^^rif:iri(?item)
                "cpt:delivered"^^rif:iri(?item ?deliverydate "ppl:John"^^rif:iri)
                "cpt:scheduled"^^rif:iri(?item ?scheduledate)
                External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration))
                External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffduration ?diffdays))
                External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))
    )
 
    Forall ?item (
        "cpt:reject"^^rif:iri("ppl:Fred"^^rif:iri ?item) :- "cpt:unsolicited"^^rif:iri(?item)
    )

  )



3 Direct Specification of syntactic forms for terms and formulas.RIF-BLD Semantics

This providesnormative section specifies the infrastructure for exchanging rule languages that support rich collectionssemantics of syntactic forms. Systems that do not support someRIF-BLD directly, without relying on RIF-FLD.

3.1 Truth Values

The set TV of that syntax directly can still support it through syntactic transformations. For instance, disjunctionstruth values in RIF-BLD consists of just two values, t and f.

3.2 Semantic Structures

The rule body can be eliminated throughkey concept in a standard transformation, such as replacing p :- Or(q r) withmodel-theoretic semantics of a pairlogic language is the notion of rules p :- q,   p :- ra semantic structure. Terms with named arguments can be reduced to positional terms by orderingThe arguments by their names and incorporating them intodefinition, below, is a little bit more general than necessary. This is done in order to better see the predicate name. For instance, p(bb->1 aa->2) can be represented as p_aa_bb(2,1) . 3.5 EBNF Grammar forconnection with the Presentation Syntaxsemantics of RIF-BLD So far,the syntax of RIF-BLD has been specified in Mathematical English. Tool developers, however, may prefer EBNF notation, which providesRIF framework.

Definition (Semantic structure). A more succinct overviewsemantic structure, I, is a tuple of the syntax. Several points should be kept in mind regarding this notation.form <TV, DTS, D, Dind, Dfunc, IC, IV, IF, Iframe, ISF, Isub, Iisa, I=, Iexternal, Itruth>. Here D is a non-empty set of elements called the syntaxdomain of first-order logicI, and Dind, Dfunc are nonempty subsets of D. Dind is not context-free, so EBNF does not captureused to interpret the syntaxelements of RIF-BLD precisely. For instance, it cannot capture the section on well-formedness conditionsConst, i.e.,which denote individuals and Dfunc is used to interpret the requirementelements of Const that each symbol in RIF-BLD can occur in at most one context.denote function symbols. As a result,before, Const denotes the EBNF grammar defines a strict supersetset of RIF-BLD (notall rules that are derivable using the EBNF grammar are well-formed rules in RIF-BLD).constant symbols and Var the EBNF syntax is not a concrete syntax: it does not addressset of all variable symbols. TV denotes the detailsset of how constants and variables are represented, and it is not sufficiently precise abouttruth values that the delimiterssemantic structure uses and escape symbols. Instead, white spaceDTS is informallythe set of primitive data types used as a delimiter, and white space is impliedin productions that use Kleene star. For instance, TERM* isI (please refer to be understood as TERM TERM ... TERM , where each ' ' abstracts from one or more blanks, tabs, newlines, etc. This is done on intentionally, since RIF's presentation syntax is intended as a toolSection Primitive Data Types of RIF-FLD for specifyingthe semantics and for illustrationof data types).


The main RIF concepts through examples. It is not intendedother components of I are total mappings defined as follows:

  1. I C maps Const to D.

    This mapping interprets constant symbols. In addition:

    • If a concrete syntax for a rule language. RIF definesconstant, c ∈ Const, denotes an individual then it is required that IC(c) ∈ Dind.
    • If c ∈ Const, denotes a concrete syntax only for exchanging rules, andfunction symbol (positional or with named arguments) then it is required that syntaxIC(c) ∈ Dfunc.
  2. IV maps Var to Dind.

    This mapping interprets variable symbols.

  3. IF maps D to functions D*ind D (here D*ind is XML-based, obtained asa refinement and serializationset of the EBNF syntax. Forall the above reasons, the EBNF syntax is not normative . 3.5.1 EBNF for RIF-BLD Condition Language The Condition Language represents formulas that can be used in the bodysequences of any finite length over the RIF-BLD rules. It is intended todomain Dind)

    This mapping interprets positional terms. In addition:

    • If d Dfunc then IF(d) must be a common part of a number of RIF dialects, including RIF PRDfunction D*ind Dind.
    • The EBNF grammar forThis means that when a superset of the RIF-BLD condition languagefunction symbol is as follows. FORMULA ::= 'And' '(' FORMULA* ')' | 'Or' '(' FORMULA* ')' | 'Exists' Var+ '(' FORMULA ')' | ATOMIC | 'External' '(' Atom ')' ATOMIC ::= Atom | Equal | Member | Subclass | Frame Atom ::= UNITERM UNITERM ::= Const '(' (TERM* | (Name '->' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '->' TERM)* ']' TERM ::= Const | Var | Expr | 'External' '(' Expr ')' Expr ::= UNITERM Const ::= '"' UNICODESTRING '"^^' SYMSPACE Name ::= UNICODESTRING Var ::= '?' UNICODESTRING The production rule forapplied to arguments that are individual object then the non-terminal FORMULA represents RIF condition formulas (defined earlier).result is also an individual object.
  4. ISF is a total mapping from D to the connectives And and Or define conjunctions and disjunctionsset of conditions, respectively. Exists introduces existentially quantified variables. Here Var+ stands for the listtotal functions of variables that are free in FORMULAthe form SetOfFiniteSets(ArgNames × Dind) D.

    RIF-BLD conditions permit only existential variables, but RIF-FLD Syntax allows arbitrary quantification, which can be usedThis mapping interprets function symbols with named arguments. In some dialects. A RIF-BLD FORMULA can alsoaddition:

    • If d Dfunc then ISF(d) must be an ATOMIC term, i.e. an Atom , External Atom , Equal , Member , Subclass , or Frame .a TERM can be a constant, variable, Expr , or External Exprfunction SetOfFiniteSets(ArgNames × Dind) Dind.
    • The RIF-BLD presentation syntax does not commitThis is analogous to any particular vocabulary except for using Unicode strings in constant symbols, as names, and for variables. Constant symbols havethe form: "UNICODESTRING"^^SYMSPACE , where SYMSPACE isinterpretation of positional terms with two differences:
      • Each pair <s,v> ArgNames × Dind represents an IRI string that identifies the symbol spaceargument/value pair instead of the constant and UNICODESTRING isjust a Unicode string fromvalue in the lexical spacecase of that symbol space. Names are just denoted by Unicode character sequences. Variables are denoted by Unicode character sequences beginning with a ?-sign. Equality, membership, and subclass terms are self-explanatory. An Atom and Expr (expression) can either bea positional or with named arguments.term.
      • The arguments of a frameterm iswith named arguments constitute a term composedfinite set of an object Id andargument/value pairs rather than a collectionfinite ordered sequence of attribute-value pairs. An External Atomsimple elements. So, the order of the arguments does not matter.
  5. Iframe is a calltotal mapping from Dind to an externally defined predicatetotal functions of RIF-DTBthe form SetOfFiniteBags(Dind × Dind) D.

    Likewise,This mapping interprets frame terms. An External Expr is a callargument, d Dind, to Iframe represent an externally defined functionobject and the finite bag {<a1,v1>, ..., <ak,vk>} represents a bag of RIF-DTBattribute-value pairs for d. Example 1 (RIF-BLD conditions). This example shows conditions thatWe will see shortly how Iframe is used to determine the truth valuation of frame terms.

    Bags (multi-sets) are composedused here because the order of atoms, expressions, frames, and existentials.the attribute/value pairs in a frame formulasis immaterial and pairs may repeat: o[a->b a->b]. Such repetitions arise naturally when variables are shown in the positions of object Ids, object properties, or property values.instantiated with constants. For brevity, we useinstance, o[?A->?B ?A->?B] becomes o[a->b a->b] if variable ?A is instantiated with the compact URI notation [ CURIE ], prefix:suffix , which shouldsymbol a and ?B with b.

  6. Isub gives meaning to the subclass relationship. It is a total function Dind × Dind D.

    The operator ## is required to be understood astransitive, i.e., c1 ## c2 and c2 ## c3 must imply c1 ## c3. This is ensured by a macrorestriction in Section Interpretation of Formulas.

  7. Iisa gives meaning to class membership. It is a total function Dind × Dind D.

    The relationships # and ## are required to have the usual property that expands intoall members of a concatenationsubclass are also members of the prefix definitionsuperclass, i.e., o # cl and suffixcl ## scl must imply o # scl. Thus, if bksThis is ensured by a prefix that expands into http://example.com/books# then bks:LeRif should be understood merely as an abbreviation for http://example.com/books#LeRifrestriction in Section Interpretation of Formulas.

  8. The compact URI notationI= is not part of the RIF-BLD syntax. Compact URI prefixes: bks expands into http://example.com/books# auth expands into http://example.com/authors# cpt expands into http://example.com/concepts# Positional terms: "cpt:book"^^rif:iri("auth:rifwg"^^rif:iri "bks:LeRif"^^rif:iri) Exists ?X ("cpt:book"^^rif:iri(?X "bks:LeRif"^^rif:iri)) Terms with named arguments: "cpt:book"^^rif:iri(cpt:author->"auth:rifwg"^^rif:iri cpt:title->"bks:LeRif"^^rif:iri) Exists ?X ("cpt:book"^^rif:iri(cpt:author->?X cpt:title->"bks:LeRif"^^rif:iri)) Frames: "bks:wd1"^^rif:iri["cpt:author"^^rif:iri->"auth:rifwg"^^rif:iri "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri] Exists ?X ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]) Exists ?X ("bks:wd2"^^rif:iri # "cpt:book"^^rif:iri["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]) Exists ?I ?X (?I["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]) Exists ?I ?X (?I # "cpt:book"^^rif:iri["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]) Exists ?S ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->"auth:rifwg"^^rif:iri ?S->"bks:LeRif"^^rif:iri]) Exists ?X ?S ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->?X ?S->"bks:LeRif"^^rif:iri]) Exists ?I ?X ?S (?I # "cpt:book"^^rif:iri[author->?X ?S->"bks:LeRif"^^rif:iri]) 3.5.2 EBNF for RIF-BLD Rule Languagea total function Dind × Dind D.

    It gives meaning to the presentation syntaxequality operator.

  9. Itruth is a total mapping D TV.

    It is used to define truth valuation for Horn rules extendsformulas.

  10. Iexternal is a mapping from the syntax in Section EBNFcoherent set of schemas for RIF-BLD Condition Language with the following productions. Group ::= 'Group' IRIMETA? '(' (RULE | Group)* ')' IRIMETA ::= Frame RULE ::= 'Forall' Var+ '(' CLAUSE ')' | CLAUSE CLAUSE ::= Implies | ATOMIC Implies ::= ATOMIC ':-' FORMULAexternally defined functions to total functions D* D. For convenient reference, we reproduceeach external schema σ = (?X1 ... ?Xn; τ) in the coherent set of such schemas associated with the conditionlanguage part, Iexternal(σ) is a function of the EBNF below. FORMULA ::= 'And' '(' FORMULA* ')' | 'Or' '(' FORMULA* ')' | 'Exists' Var+ '(' FORMULA ')' | ATOMIC | 'External' '(' Atom ')' ATOMIC ::= Atom | Equal | Member | Subclass | Frame Atom ::= UNITERM UNITERM ::= Const '(' (TERM* | (Name '->' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '->' TERM)* ']' TERM ::= Const | Var | Expr | 'External' '(' Expr ')' Expr ::= UNITERM Const ::= '"' UNICODESTRING '"^^' SYMSPACE Name ::= UNICODESTRING Var ::= '?' UNICODESTRING A RIF-BLD Group is a nested collection of RIF-BLD rules annotated with optional metadata, IRIMETAform Dn D.

    For every external schema, σ, represented as Frame s. A Group can contain any number of RULE s alongassociated with any number of nested Group s. Rules are generated by CLAUSE , which canthe language, Iexternal(σ) is assumed to be specified externally in some document (hence the scope of a Forall quantifier.name external schema). In particular, if σ is a CLAUSE in the RULE production hasschema of a free (non-quantified) variable, it must occurRIF builtin predicate or function, Iexternal(σ) is specified in the Var+ sequence. Frame , Var , ATOMIC ,document Data Types and FORMULA were defined as partBuiltins so that:

    • If σ is a schema of a builtin function then Iexternal(σ) must be the syntax for positive conditions in Section EBNF for RIF-BLD Condition Language .function defined in the CLAUSE production an ATOMIC is treated as a rule with an empty condition part -- in which case itaforesaid document.
    • If σ is usually calleda fact . Note that, byschema of a definition in Section Formulas , formulas that query externally defined atoms (i.e., formulas of the form External(Atom(...)) ) are not allowed in the conclusion part of a rulebuiltin predicate then Itruth ο ( ATOMIC does not expand toIexternal ). Example 2 (RIF-BLD rules). This example shows a business rule borrowed from the document RIF Use Cases and Requirements : If an item is perishable(σ)) (the composition of Itruth and it is delivered to John more than 10 days after the scheduled delivery date then the item willIexternal(σ), a truth-valued function) must be rejected by him.as before,specified in Data Types and Builtins.

For better readabilityconvenience, we use the compact URI notation. Compact URI prefixes: ppl expands into http://example.com/people# cpt expands into http://example.com/concepts# op expands intoalso define the yet-to-be-determined IRI for RIF builtin predicates a. Universal form: Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdaysfollowing mapping I from terms to D:

  • I( "cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item) :- And("cpt:perishable"^^rif:iri(?item) "cpt:delivered"^^rif:iri(?item ?deliverydate "ppl:John"^^rif:iri) "cpt:scheduled"^^rif:iri(?item ?scheduledate) External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration)) External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffduration ?diffdays)) External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))k) b. Universal-existential form: Forall ?item= IC( "cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item ) :- Exists ?deliverydate ?scheduledate ?diffduration ?diffdaysk), if k is a symbol in Const
  • I( And("cpt:perishable"^^rif:iri(?item) "cpt:delivered"^^rif:iri(?item ?deliverydate "ppl:John"^^rif:iri) "cpt:scheduled"^^rif:iri(?item ?scheduledate) External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration)) External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffduration ?diffdays)) External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer))) )?v) Example 3 (A RIF-BLD group annotated with metadata). This example shows a group formula that consists of two RIF-BLD rules. The first of these rules is copied from Example 2a. The group= IV(?v), if ?v is annotated with Dublin Core metadata represented asa frame. Compact URI prefixes: bks expands into http://example.com/books# auth expands into http://example.com/authors# cpt expands into http://example.com/concepts# dc expands into http://dublincore.org/documents/dces/ w3 expands into http://www.w3.org/ Group " http://sample.org "^^rif:iri["dc:publisher"^^rif:iri->"w3:W3C"^^rif:iri "dc:date"^^rif:iri->"2008-04-04"^^xsd:date] ( Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays ( "cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item) :- And("cpt:perishable"^^rif:iri(?item) "cpt:delivered"^^rif:iri(?item ?deliverydate "ppl:John"^^rif:iri) "cpt:scheduled"^^rif:iri(?item ?scheduledate) External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration)) External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffduration ?diffdays)) External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer))) ) Forall ?itemvariable in Var
  • I( "cpt:reject"^^rif:iri("ppl:Fred"^^rif:iri ?item) :- "cpt:unsolicited"^^rif:iri(?item)f(t1 ... tn)) 4 Direct Specification of RIF-BLD Semantics This normative section specifies the semantics of RIF-BLD directly, without referring to RIF-FLD. 4.1 Truth Values The set TV of truth values in RIF-BLD consists of just two values, t and f . 4.2 Semantic Structures The key concept in a model-theoretic semantics of a logic language is the notion of a semantic structure . The definition, below, is a little bit more general than necessary. This is done in order to better see the connection with the semantics of the RIF framework . Definition (Semantic structure) . A semantic structure , I , is a tuple of the form < TV , DTS , D , D ind , D func , I C ,= I V ,F(I(f ,))(I frame ,(t1),...,I SF ,(tn))
  • I sub ,(f(s1->v1 ... sn->vn)) = I isa ,SF(I =(f))({<s1,I external(v1)>,...,<sn,I truth >.(vn)>})
  • Here D iswe use {...} to denote a non-emptyset of elements called the domainargument/value pairs.

  • I(o[a1->v1 ... ak->vk]) = Iframe(I(o))({<I(a1),I(v1)>, ..., <I(an),I(vn)>})
  • Here {...} denotes a bag of attribute/value pairs.

  • I , and D ind , D func are nonempty subsets(c1##c2) = Isub(I(c1), I(c2))
  • I(o#c) = Iisa(I(o), I(c))
  • I(x=y) = I=(I(x), I(y))
  • I(External(t)) = Iexternsl(σ)(I(s1), ..., I(sn)), if t is an instance of Dthe external schema σ = (?X1 ... ?Xn; τ) by substitution ?X1/s1 ... ?Xn/s1.

    D indNote that, by definition, External(t) is used to interpret the elements of Const , which denote individuals and D funcwell formed only if t is used to interpret the elementsan instance of Const that denote function symbols. As before, Const denotesan external schema. Furthermore, by the setdefinition of all constant symbols and Var the setcoherent sets of all variable symbols. TV denotes the setexternal schemas, t can be an instance of truth values that the semantic structure uses and DTSat most one such schema, so I(External(t)) is well-defined.

The seteffect of primitivedata types. The data types usedin I (please refer to Section PrimitiveDTS impose the following restrictions. If dt is a symbol space identifier of a data Typestype, let LSdt denote the lexical space of RIF-FLD fordt, VSdt denote its value space, and Ldt: LSdt VSdt the semanticslexical-to-value-space mapping (for the definitions of these concepts, see Section Primitive Data types). The other componentsTypes of I are total mappings defined as follows: I C maps Const toRIF-FLD). Then the following must hold:

  • VSdt D . This mapping interpretsind; and
  • For each constant symbols. In addition: If a constant, c  ∈  Const"lit"^^dt LSdt, denotes an individual then it is required thatIC( c ) ∈  D ind . If c  ∈  Const , denotes a function symbol (positional or with named arguments) then it is required"lit"^^dt) = Ldt(lit).

That is, IC ( c ) ∈  D funcmust map the constants of a data type dt in accordance with Ldt.

RIF-BLD does not impose restrictions on I V maps VarC for constants in the lexical spaces that do not correspond to D indprimitive datatypes in DTS. This mapping interprets variable symbols. I F maps D to functions D* ind D (here D* ind is a set of all sequences  ☐

3.3 Interpretation of any finite length overFormulas

Definition (Truth valuation). Truth valuation for well-formed formulas in RIF-BLD is determined using the domain D ind ) This mapping interpretsfollowing function, denoted TValI:

  1. Positional terms. In addition: If d D func thenatomic formulas: TValI F( dr(t1 ... tn) must be a function D* ind D ind . This means that when a function symbol is applied to) = Itruth(I(r(t1 ... tn)))
  2. Atomic formulas with named arguments: TValI(p(s1->v1 ... sk->vk)) = Itruth(I(p(s1->v1 ... sk->vk))).
  3. Equality: TValI(x = y) = Itruth(I(x = y)).
    • To ensure that are individual object thenequality has precisely the resultexpected properties, it is also an individual object.required that:
      I SF is a total mapping from D to the set of total functions of the form SetOfFiniteSetstruth( ArgNames × D ind ) D . This mapping interprets function symbols with named arguments. In addition:I(x = y)) = t if and only if d D func thenI SF( dx) must be a function SetOfFiniteSets= I( ArgNames × D indy) D ind .and that Itruth(I(x = y)) = f otherwise.
    • This is analogoustantamount to saying that TValI(x = y) = t if I(x) = I(y).
  4. Subclass: TValI(sc ## cl) = Itruth(I(sc ## cl)).

    To ensure that the interpretation of positional terms with two differences: Each pair < s,v > ArgNames × D ind represents an argument/value pair instead of just a value in the case of a positional term. The arguments of a term with named arguments constitute a finite set of argument/value pairs rather than a finite ordered sequence of simple elements. So, the order of the arguments does not matter. I frameoperator ## is a total mapping from D ind to total functions oftransitive, i.e., c1 ## c2 and c2 ## c3 imply c1 ## c3, the form SetOfFiniteBags ( D ind × D ind ) D . This mapping interprets frame terms. An argument, dfollowing is required:

    For all c1, c2, c3D ind, to  if TValI frame represent an object and the finite bag {< a1,v1 >, ..., < ak,vk >} represents a bag of attribute-value pairs for d(c1 ## c2) = TValI(c2 ## c3) = t   then TValI(c1 ## c3) = t.
  5. We will see shortly howMembership: TValI(o # cl) = I frame is used to determine thetruth valuation of frame terms. Bags (multi-sets) are used here because the order(I(o # cl)).

    To ensure that all members of the attribute/value pairs ina frame is immaterial and pairs may repeat: o[a->b a->b] . Such repetitions arise naturally when variablessubclass are instantiated with constants. For instance, o[?A->?B ?A->?B] becomes o[a->b a->b] if variable ?A is instantiated withalso members of the symbol asuperclass, i.e., o # cl and ?B with b . I sub gives meaning tocl ## scl implies o # scl, the subclass relationship. Itfollowing is a total functionrequired:

    For all o, cl, scl D ind × D ind D . The operator ## is required to be transitive, i.e., c1 ## c2 and c2 ## c3 must imply c1 ## c3 . This is ensured by a restriction in Section Interpretation of Formulas .,   if TValI isa gives meaning to class membership. It is a total function D ind × D ind D . The relationships # and ## are required to have the usual property that all members of a subclass are also members of the superclass, i.e.,(o # cl and) = TValI(cl ## scl must imply o # scl . This is ensured by a restriction in Section Interpretation of Formulas .) = t   then   TValI(o # scl) = is a total function D ind × D ind Dt.
  6. It gives meaning to the equality operator.Frame: TValI truth is(o[a1->v1 ... a total mapping D TV . It is used to definek->vk]) = Itruth valuation for formulas.(I external is(o[a1->v1 ... a mapping fromk->vk])).

    Since the coherent set of schemas for externally defined functionsdifferent attribute/value pairs are supposed to total functions D * D . For each external schema σ = (?X 1 ... ?X n ; τ) in the coherent set of such schemas associated withbe understood as conjunctions, the language ,following is required:

    TValI external( σ ) iso[a1->v1 ... a function of the form D n D . For every external schema, σ , associated with the language, I external ( σk->vk]) is assumed to be specified externally in some document (hence the name external schema ). In particular,= t if σ is a schema of a RIF builtin predicate or function, I external ( σ ) is specified in the document Data Typesand Builtins so that: If σ is a schema of a builtin function then I external ( σ ) must be the function defined in the aforesaid document.only if σ is a schema of a builtin predicate then I truth ο ( I external ( σ )) (the composition of I truth and I external ( σ ), a truth-valued function) must be as specified in Data Types and Builtins . For convenience, we also define the following mapping I from terms to D :TValI( ko[a1->v1]) = ... = TValI C(o[ak ), if->vk is a symbol in Const I ( ?v]) = I V ( ?v ), if ?v is a variable in Vart.
  7. Externally defined atomic formula: TValI( f(t 1 ... t n )External(t)) = I Ftruth(Iexternal( f ))(σ)(I( ts1 ),...,), ..., I(sn))), if t is an atomic formula that is an instance of the external schema σ = (?X1 ... ?Xn )) I ( f(s; τ) by substitution ?X1 ->v/s1 ... s n ->v... ?Xn ) ) = I SF ( I ( f ))({< s 1 , I ( v 1 )>,...,< s n , I ( v n )>}) Here we use {...} to denote a set of argument/value pairs. I ( o[a 1 ->v 1 ... a k ->v k ] ) = I frame ( I ( o ))({< I ( a 1 ), I ( v 1 )>, ..., < I ( a n ), I ( v n )>}) Here {...} denotes a bag of attribute/value pairs. I ( c1##c2 ) = I sub ( I ( c1 ), I ( c2 )) I ( o#c ) = I isa ( I ( o ), I ( c )) I ( x=y ) = I = ( I (x), I (y)) I ( External(t) ) = I externsl ( σ )( I ( s 1 ), ..., I ( s n )), if t is an instance of the external schema σ = (?X 1 ... ?X n ; τ) by substitution ?X 1 /s 1 ... ?X n /s/s1.

    Note that, by definition, External(t) is well formedwell-formed only if t is an instance of an external schema. Furthermore, by the definition of coherent sets of external schemas, t can be an instance of at most one such schema, so I(External(t)) is well-defined.

  8. The effect of data types. The data types in DTS impose the following restrictions. If dt is a symbol space identifier of a data type, let LS dt denote the lexical space of dt , VS dt denote its value space, and L dtConjunction: LS dt VS dt the lexical-to-value-space mapping (for the definitions of these concepts, see Section Primitive Data Types of RIF-FLD). Then the following must hold: VS dt D ind ; and For each constant "lit"^^dt LS dt ,TValI C( "lit"^^dt ) = L dt ( lit ). That is, I C must map the constants of a data type dt in accordance with L dt . RIF-BLD does not impose restrictions on IAnd(c for constants in the lexical spaces that do not correspond to primitive datatypes in DTS .   ☐ 4.3 Interpretation of Formulas Definition (Truth valuation) . Truth valuation for well-formed formulas in RIF-BLD is determined using the following function, denoted TVal I : Positional atomic formulas : TVal I ( r(t1 ... tcn)) = t if and only if TValI truth ( I ( r(t(c1) = ... t= TValI(cn) )) Atomic formulas with named arguments := t. Otherwise, TValI( p(s 1 ->vAnd(c1 ... s k ->v kcn)) = f.
  9. The empty conjunction is treated as a tautology, so TValI truth(And()) = t.

  10. Disjunction: TValI( p(s 1 ->vOr(c1 ... s k ->v kcn) )). Equality :) = f if and only if TValI ( x = y(c1) = ... = TValI truth ((cn) = f. Otherwise, TValI( x = y )). To ensure that equality has preciselyOr(c1 ... cn)) = t.
  11. The expected properties, itempty disjunction is required that:treated as a contradiction, so TValI truth(Or()) = f.

  12. Quantification:
    • TValI( x = y ))Exists ?v1 ... ?vn (φ)) = t if and only if for some I*, described below, TValI*( xφ) = t.
    • TValI( y )Forall ?v1 ... ?vn (φ)) = t if and that I truth (only if for every I ( x = y )) = f otherwise. This is tantamount to saying that*, described below, TVal II*( x = yφ) = t if.

    Here I (x) =* is a semantic structure of the form <TV, DTS, D, Dind, Dfunc, I (y). Subclass : TValC, I*V, IF, Iframe, ISF, Isub, Iisa, I ( sc ## cl )=, Iexternsl, Itruth (>, which is exactly like I ( sc ## cl )). To ensure, except that the operator ## is transitive, i.e., c1 ## c2 and c2 ## c3 imply c1 ## c3mapping I*V, the followingis required: For all c1 , c2 , c3 D ,used instead of IV.   ifI*V is defined to coincide with IV on all variables except, possibly, on ?v1,...,?vn.

  13. Rule implication:
    • TValI( c1 ## c2conclusion :- condition) = t, if either TValI( c2 ## c3conclusion)=t or TValI(condition)=f.
    • TValI(conclusion :- condition) = tf   otherwise.
  14. Groups of rules:

    If Γ is a group formula of the form Group φ 1 ... ρn) or Group 1 ... ρn) then

    • TValI( c1 ## c3Γ) = t . Membership :if and only if TValI( o # clρ1) = t, ..., TValI truth(ρn) = t.
    • TValI( o # cl )). To ensureΓ) = f   otherwise.

    This means that all members ofa subclass are also membersgroup of rules is treated as a conjunction. The superclass, i.e., o # cl and cl ## scl implies o # scl , the followingmetadata is required:ignored for all o , cl , scl Dpurposes of the RIF-BLD semantics.

A model of a group of rules, Γ,   if TValis a semantic structure I ( o # cl ) =such that TValI( cl ## sclΓ) = t   then   TVal. In this case, we write I ( o # scl ) = t |= Γ.   ☐

Note that although metadata associated with RIF-BLD formulas is ignored by the semantics, it can be extracted by XML tools. Since metadata is represented by frame : TVal I ( o[a 1 ->v 1 ...terms, it can be reasoned with by RIF-BLD rules.

3.4 Logical Entailment

We now define what it means for a k ->v k ] ) = I truth ( I ( o[a 1 ->v 1 ...set of RIF-BLD rules to entail a k ->v k ] )). SinceRIF-BLD condition. We say that a RIF-BLD condition formula φ is existentially closed, if and only if every variable, ?V, in φ occurs in a subformula of the different attribute/value pairs are supposed toform Exists ...?V...(ψ).

Definition (Logical entailment). Let Γ be understood as conjunctions, the following is required: TVal I ( o[a 1 ->v 1 ...a k ->v k ] ) = tRIF-BLD group formula and φ an existentially closed RIF-BLD condition formula. We say that Γ entails φ, written as Γ |= φ, if and only if for every model of Γ it is the case that TValI( o[a 1 ->v 1 ] ) = ... = TVal I ( o[a k ->v k ]φ) = t.

Externally defined atomic formula : TVal I ( External(t) ) = I truth ( I external ( σ )( I ( s 1 ), ...,Equivalently, we can say that Γ |= φ holds iff whenever I ( s n ))), if t is an atomic formula |= Γ it follows that is an instance of the external schema σ = (?X 1 ... ?X n ; τ) by substitution ?X 1 /s 1 ... ?X n /s 1also I |= φ. Note that, by definition, External(t) is well-formed only if t  ☐


4 XML Serialization Syntax for RIF-BLD

The XML serialization for RIF-BLD is an instance of an external schema. Furthermore, byalternating or fully striped [ANF01]. A fully striped serialization views XML documents as objects and divides all XML tags into class descriptors, called type tags, and property descriptors, called role tags. We use capitalized names for type tags and lowercase names for role tags.


4.1 XML for the definitionRIF-BLD Condition Language

XML serialization of coherent setsthe presentation syntax of Section EBNF for RIF-BLD Condition Language uses the following tags.

- 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)
- External   schemas , t can be(external call, containing a content role)
- content   (content role, containing an  instance of at most one such schema, so I ( External(t) ) is well-defined. Conjunction : TVal I ( And( c 1 ... c n ) ) = t ifAtom, for predicates, or Expr, for functions)
- Member    (member formula)
- Subclass  (subclass formula)
- Frame     (Frame formula)
- object    (Member/Frame role, containing a TERM or an object description)
- op        (Atom/Expr role for predicates/functions as operations)
- arg       (positional argument role)
- upper     (Member/Subclass upper class role)
- lower     (Member/Subclass lower instance/class role)
- slot      (Atom/Expr/Frame slot role, containing a Prop)
- Prop      (Property, prefix version of slot infix '->')
- key       (Prop key role, containing a Const)
- val       (Prop val role, containing a TERM)
- Equal     (prefix version of term equation '=')
- Expr      (expression formula, positional or with named arguments)
- side      (Equal left-hand side and  only if TVal I (c 1 ) = ... = TVal I (c n ) = t . Otherwise, TVal I ( And( c 1 ... c n ) ) = fright-hand side role)
- Const     (individual, function, or predicate symbol, with optional 'type' attribute)
- Name      (name of named argument)
- Var       (logic variable)


For the XML Schema Definition (XSD) of the RIF-BLD condition language see Appendix XML Schema for BLD.

The empty conjunction is treatedXML syntax for symbol spaces utilizes the type attribute associated with XML term elements such as Const. For instance, a tautology, so TVal I ( And() ) = tliteral in the xsd:dateTime data type can be represented as <Const type="xsd:dateTime">2007-11-23T03:55:44-02:30</Const>.


Disjunction : TVal I ( Or( c 1 ... c n ) ) = f ifExample 4 (A RIF condition and only if TVal I (c 1 ) = ... = TVal I (c n ) = f . Otherwise, TVal I ( Or( c 1 ... c n ) ) = t .its XML serialization).

This example illustrates XML serialization for RIF conditions. As before, the empty disjunctioncompact URI notation is treated as a contradiction, so TVal I ( Or() ) = f . Quantification : TVal I ( Exists ?v 1 ... ?v n (φ) ) = t if and only ifused for some I *, described below, TVal I* ( φ ) = t . TVal I ( Forall ?v 1 ... ?v n (φ)) = t ifbetter readability.

Compact URI prefixes:

  bks  expands into http://example.com/books#
  cpt  expands into http://example.com/concepts#
  curr expands into http://example.com/currencies#
RIF condition

   And  only if for every I *, described below, TVal I* ( φ(Exists ?Buyer ("cpt:purchase"^^rif:iri(?Buyer
                                               ?Seller
                                               "cpt:book"^^rif:iri(?Author "bks:LeRif"^^rif:iri)
                                               "curr:USD"^^rif:iri("49"^^xsd:integer)))
        ?Seller=?Author )

 = t . Here I * is a semantic structureXML serialization

   <And>
     <formula>
       <Exists>
         <declare><Var>Buyer</Var></declare>
         <formula>
           <Atom>
             <op><Const type="rif:iri">cpt:purchase</Const></op>
             <arg><Var>Buyer</Var></arg>
             <arg><Var>Seller</Var></arg>
             <arg>
               <Expr>
                 <op><Const type="rif:iri">cpt:book</Const></op>
                 <arg><Var>Author</Var></arg>
                 <arg><Const type="rif:iri">bks:LeRif</Const></arg>
               </Expr>
             </arg>
             <arg>
               <Expr>
                 <op><Const type="rif:iri">curr:USD</Const></op>
                 <arg><Const type="xsd:integer">49</Const></arg>
               </Expr>
             </arg>
           </Atom>
         </formula>
       </Exists>
     </formula>
     <formula>
       <Equal>
         <side><Var>Seller</Var></side>
         <side><Var>Author</Var></side>
       </Equal>
     </formula>
   </And>


Example 5 (A RIF condition with named arguments and its XML serialization).

This example illustrates XML serialization of the form < TV , DTS , D , D ind , D func , I C , I * V , I F , I frame , I SF , I sub , I isa , I = , I externsl , I truth >, which is exactly like I , exceptRIF conditions that the mapping I * V , is used instead of I V .   I * V is defined to coincideinvolve terms with I V on all variables except, possibly, on ?v 1 ,..., ?v n . Rule implication : TVal I ( conclusion  :- condition ) = t , if either TVal I ( conclusion )= t or TVal I ( condition )= f . TVal Inamed arguments.

Compact URI prefixes:

  bks  expands into http://example.com/books#
  auth expands into http://example.com/authors#
  cpt  expands into http://example.com/concepts#
  curr expands into http://example.com/currencies#
RIF condition:

   And (Exists ?Buyer ?P (
                  conclusion  :-?P#"cpt:purchase"^^rif:iri["cpt:buyer"^^rif:iri->?Buyer
                                            "cpt:seller"^^rif:iri->?Seller
                                            "cpt:item"^^rif:iri->"cpt:book"^^rif:iri(cpt:author->?Author
                                                                                     cpt:title->"bks:LeRif"^^rif:iri)
                                            "cpt:price"^^rif:iri->"49"^^xsd:integer
                                            "cpt:currency"^^rif:iri->"curr:USD"^^rif:iri])
        ?Seller=?Author)


XML serialization:

   <And>
     <formula>
       <Exists>
         <declare><Var>Buyer</Var></declare>
         <declare><Var>P</Var></declare>
         <formula>
           <Frame>
             <object>
               <Member>
                 <lower><Var>P</Var></lower>
                 <upper><Const type="rif:iri">cpt:purchase</Const></upper>
               </Member>
             </object>
             <slot>
               <Prop>
                 <key><Const type="rif:iri">cpt:buyer</Const></key>
                 <val><Var>Buyer</Var></val>
               </Prop>
             </slot>
             <slot>
               <Prop>
                 <key><Const type="rif:iri">cpt:seller</Const></key>
                 <val><Var>Seller</Var></val>
               </Prop>
             </slot>
             <slot>
               <Prop>
                 <key><Const type="rif:iri">cpt:item</Const></key>
                 <val>
                   <Expr>
                     <op><Const type="rif:iri">cpt:book</Const></op>
                     <slot>
                       <Prop>
                         <key><Name>cpt:author</Name></key>
                         <val><Var>Author</Var></val>
                       </Prop>
                     </slot>
                     <slot>
                       <Prop>
                         <key><Name>cpt:title</Name></key>
                         <val><Const type="rif:iri">bks:LeRif</Const></val>
                       </Prop>
                     </slot>
                   </Expr>
                 </val>
               </Prop>
             </slot>
             <slot>
               <Prop>
                 <key><Const type="rif:iri">cpt:price</Const></key>
                 <val><Const type="xsd:integer">49</Const></val>
               </Prop>
             </slot>
             <slot>
               <Prop>
                 <key><Const type="rif:iri">cpt:currency</Const></key>
                 <val><Const type="rif:iri">curr:USD</Const></val>
               </Prop>
             </slot>
           </Frame>
         </formula>
       </Exists>
     </formula>
     <formula>
       <Equal>
         <side><Var>Seller</Var></side>
         <side><Var>Author</Var></side>
       </Equal>
     </formula>
   </And>


4.2 XML for the RIF-BLD Rule Language

We now extend the RIF-BLD serialization from Section XML for RIF-BLD Condition ) = f   otherwise. Groups ofLanguage by including rules : If Γ is a group formula of the form Group φ 1 ... ρ n ) or Group 1 ... ρ n ) then TVal I ( Γ ) = t if and only if TVal I ( ρ 1 ) = t , ..., TVal I ( ρ n ) = tas described in Section EBNF for RIF-BLD Rule Language. TVal I ( Γ ) = f   otherwise. This means that aThe extended serialization uses the following additional tags.


- Group    (nested collection of  rulessentences annotated with metadata)
- meta     (meta role, containing metadata, which is  treatedrepresented as a  conjunction. The metadata is ignoredFrame)
- sentence (sentence role, containing RULE or Group)
- Forall   (quantified formula for  purposes of'Forall', containing declare and formula roles)
- Implies  (implication, containing if and then roles)
- if       (antecedent role, containing FORMULA)
- then     (consequent role, containing ATOMIC)


The RIF-BLD semantics. A model of a groupXML Schema Definition of rules, Γ , is a semantic structure I such that TVal I ( Γ ) = t . In this case, we write I   |= Γ .   ☐ Note that although metadata associated withRIF-BLD formulasis ignored by the semantics, it can be extracted bygiven in Appendix XML tools. Since metadata is represented by frame terms, it can be reasoned with by RIF-BLD rules. 4.4 Logical Entailment We now define what it meansSchema for a set of RIF-BLD rules to entailBLD.


Example 6 (Serializing a RIF-BLD condition. We say thatgroup annotated with metadata).

This example shows a RIF-BLD condition formula φserialization for the group from Example 3. For convenience, the group is existentially closed , if and only if every variable, ?V , in φ occurs in a subformula ofreproduced at the form Exists ...?V...(ψ) . Definition (Logical entailment). Let Γ be a RIF-BLD group formula and φ an existentially closed RIF-BLD condition formula. We say that Γ entails φ , written as Γ |= φ , iftop and only if for every model of Γ itthen is the case that TVal Ifollowed by its serialization.

Compact URI prefixes:

  bks  expands into http://example.com/books#
  auth expands into http://example.com/authors#
  cpt  expands into http://example.com/concepts#
  dc   expands into http://dublincore.org/documents/dces/
  w3   expands into http://www.w3.org/
Presentation syntax:

   Group "http://sample.org"^^rif:iri["dc:publisher"^^rif:iri->"w3:W3C"^^rif:iri
                                      "dc:date"^^rif:iri->"2008-04-04"^^xsd:date]
    (

         φForall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays (
            "cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item) :-
                And("cpt:perishable"^^rif:iri(?item)
                    "cpt:delivered"^^rif:iri(?item ?deliverydate "ppl:John"^^rif:iri)
                    "cpt:scheduled"^^rif:iri(?item ?scheduledate)
                    External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration))
                    External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffduration ?diffdays))
                    External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))
        )
 
        Forall ?item (
            "cpt:reject"^^rif:iri("ppl:Fred"^^rif:iri ?item) :- "cpt:unsolicited"^^rif:iri(?item)
        )

    )


 = t . Equivalently, we can say that Γ |= φ holds iff whenever I   |=   Γ it follows that also I   |= φ .   ☐ 5 XML Serialization Syntax for RIF-BLD The XML serialization for RIF-BLD is alternating or fully striped [ ANF01 ]. A fully striped serialization views XML documents as objects and divides all XML tags into class descriptors, called type tags , and property descriptors, called role tags . We use capitalized names for type tags and lowercase names for role tags. 5.1 XML for RIF-BLD Condition LanguageXML  serialization of the presentation syntax of Section EBNF for RIF-BLD Condition Language uses the following tags. - 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) - External (external call, containing a content role) - content (content role, containing an Atom, for predicates, or Expr, for functions) - Member (member formula) - Subclass (subclass formula) - Frame (Frame formula) - object (Member/Frame role, containing a TERM or an object description) - op (Atom/Expr role for predicates/functions as operations) - arg (positional argument role) - upper (Member/Subclass upper class role) - lower (Member/Subclass lower instance/class role) - slot (Atom/Expr/Frame slot role, containing a Prop) - Prop (Property, prefix version of slot infix '->') - key (Prop key role, containing a Const) - val (Prop val role, containing a TERM) - Equal (prefix version of term equation '=') - Expr (expression formula, positional or with named arguments) - side (Equal left-hand sidesyntax:

   <Group>
    <meta>
      <Frame>
        <object>
          <Const type="rif:iri">http://sample.org</Const>
        </object>
        <slot>
          <Prop>
            <key><Const type="rif:iri">dc:publisher</Const></key>
            <val><Const type="rif:iri">w3:W3C</Const></val>
          </Prop>
        </slot>
        <slot>
          <Prop>
            <key><Const type="rif:iri">dc:date</Const></key>
            <val><Const type="xsd:date">2008-04-04</Const></val>
          </Prop>
        </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>
                   <arg><Var>item</Var></arg>
                 </Atom>
               </formula>
               <formula>
                 <Atom>
                   <op><Const type="rif:iri">cpt:delivered</Const></op>
                   <arg><Var>item</Var></arg>
                   <arg><Var>deliverydate</Var></arg>
                   <arg><Const type="rif:iri">ppl:John</Const></arg>
                 </Atom>
               </formula>
               <formula>
                 <Atom>
                   <op><Const type="rif:iri">cpt:scheduled</Const></op>
                   <arg><Var>item</Var></arg>
                   <arg><Var>scheduledate</Var></arg>
                 </Atom>
               </formula>
               <formula>
                 <External>
                   <content>
                     <Atom>
                       <op><Const type="rif:iri">fn:subtract-dateTimes-yielding-dayTimeDuration</Const></op>
                       <arg><Var>deliverydate</Var></arg>
                       <arg><Var>scheduledate</Var></arg>
                       <arg><Var>diffduration</Var></arg>
                     </Atom>
                   </content>
                 </External>
               </formula>
               <formula>
                 <External>
                   <content>
                     <Atom>
                       <op><Const type="rif:iri">fn:get-days-from-dayTimeDuration</Const></op>
                       <arg><Var>diffduration</Var></arg>
                       <arg><Var>diffdays</Var></arg>
                     </Atom>
                   </content>
                 </External>
               </formula>
               <formula>
                 <External>
                   <content>
                     <Atom>
                       <op><Const type="rif:iri">op:numeric-greater-than</Const></op>
                       <arg><Var>diffdays</Var></arg>
                       <arg><Const type="xsd:long">10</Const></arg>
                     </Atom>
                   </content>
                 </External>
               </formula>
             </And>
           </if>
           <then>
             <Atom>
               <op><Const type="xsd:long">reject</Const></op>
               <arg><Const type="rif:iri">ppl:John</Const></arg>
               <arg><Var>item</Var></arg>
             </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>
               <arg><Var>item</Var></arg>
             </Atom>
           </if>
           <then>
             <Atom>
               <op><Const type="rif:iri">cpt:reject</Const></op>
               <arg><Const type="rif:iri">ppl:Fred</Const></arg>
               <arg><Var>item</Var></arg>
             </Atom>
           </then>
         </Implies>
       </formula>
     </Forall>
    </sentence>
   </Group>


4.3 Translation Between the RIF-BLD Presentation and right-hand side role) - Const (individual, function, or predicate symbol, with optional 'type' attribute) - Name (name of named argument) - Var (logic variable) ForXML Syntaxes

We now show how to translate between the presentation and XML Schema Definition (XSD)syntaxes of RIF-BLD.

4.3.1 Translation of the RIF-BLD Condition Language

see Appendix XML Schema for BLD .The XMLtranslation between the presentation syntax for symbol spaces utilizesand the type attribute associated withXML term elements such as Const . For instance, a literalsyntax of the RIF-BLD Condition Language is specified by the table below. Since the presentation syntax of RIF-BLD is context sensitive, the translation must differentiate between the terms that occur in the xsd:dateTime data type can be representedposition of the individuals from terms that occur as <Const type="xsd:dateTime">2007-11-23T03:55:44-02:30</Const> . Example 4 (A RIF condition and its XML serialization).atomic formulas. To this example illustrates XML serialization for RIF conditions. As before,end, in the compact URI notation is used for better readability. Compact URI prefixes: bks expands into http://example.com/books# cpt expands into http://example.com/concepts# curr expands into http://example.com/currencies# RIF conditiontranslation table, the positional and (Exists ?Buyer ("cpt:purchase"^^rif:iri(?Buyer ?Seller "cpt:book"^^rif:iri(?Author "bks:LeRif"^^rif:iri) "curr:USD"^^rif:iri("49"^^xsd:integer))) ?Seller=?Authornamed 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(...).

The prime symbol (for instance, variable') indicates that the translation function defined by the table must be applied recursively (i.e., to variable in our example).

Presentation Syntax XML serializationSyntax
And (
  conjunct1
  . . .
  conjunctn
    )
<And>
  <formula>conjunct1'</formula>
   . . .
  <formula>conjunctn'</formula>
</And>
Or (
  disjunct1
  . . .
  disjunctn
   )
<Or>
  <formula>disjunct1'</formula>
   . . .
  <formula>disjunctn'</formula>
</Or>
Exists
  variable1
  . . .
  variablen (
             body
            )
<Exists>
   <declare><Var>Buyer</Var></declare><declare>variable1'</declare>
   . . .
  <declare>variablen'</declare>
  <formula>body'</formula>
</Exists>
pred (
  argument1
  . . .
  argumentn
     )
<Atom>
   <op><Const type="rif:iri">cpt:purchase</Const></op> <arg><Var>Buyer</Var></arg> <arg><Var>Seller</Var></arg><op>pred'</op>
  <arg> <Expr> <op><Const type="rif:iri">cpt:book</Const></op> <arg><Var>Author</Var></arg> <arg><Const type="rif:iri">bks:LeRif</Const></arg> </Expr>argument1'</arg>
   . . .
  <arg>  <Expr> <op><Const type="rif:iri">curr:USD</Const></op> <arg><Const type="xsd:integer">49</Const></arg> </Expr>argumentn'</arg>
</Atom>
 </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And> Example 5 (A RIF condition and its XML serialization). This example illustrates XML serialization of RIF conditions that involve terms with named arguments. Compact URI prefixes: bks expands into http://example.com/books# auth expands into http://example.com/authors# cpt expands into http://example.com/concepts# curr expands into http://example.com/currencies# RIF condition: And (Exists ?Buyer ?PExternal (
   ?P#"cpt:purchase"^^rif:iri["cpt:buyer"^^rif:iri->?Buyer "cpt:seller"^^rif:iri->?Seller "cpt:item"^^rif:iri->"cpt:book"^^rif:iri(cpt:author->?Author cpt:title->"bks:LeRif"^^rif:iri) "cpt:price"^^rif:iri->"49"^^xsd:integer "cpt:currency"^^rif:iri->"curr:USD"^^rif:iri]) ?Seller=?Author) XML serialization: <And> <formula> <Exists> <declare><Var>Buyer</Var></declare> <declare><Var>P</Var></declare> <formula> <Frame> <object> <Member> <lower><Var>P</Var></lower> <upper><Const type="rif:iri">cpt:purchase</Const></upper> </Member> </object> <slot> <Prop> <key><Const type="rif:iri">cpt:buyer</Const></key> <val><Var>Buyer</Var></val> </Prop> </slot> <slot> <Prop> <key><Const type="rif:iri">cpt:seller</Const></key> <val><Var>Seller</Var></val> </Prop> </slot> <slot> <Prop> <key><Const type="rif:iri">cpt:item</Const></key> <val>atomexpr
         )
<External>
  <content>atomexpr'</content>
</External>
func (
  argument1
  . . .
  argumentn
     )
<Expr>
   <op><Const type="rif:iri">cpt:book</Const></op> <slot> <Prop> <key><Name>cpt:author</Name></key> <val><Var>Author</Var></val> </Prop> </slot> <slot> <Prop> <key><Name>cpt:title</Name></key> <val><Const type="rif:iri">bks:LeRif</Const></val> </Prop> </slot><op>func'</op>
  <arg>argument1'</arg>
   . . .
  <arg> argumentn'</arg>
</Expr>
 </val> </Prop> </slot>pred (
  unicodestring1 -> filler1
  . . .
  unicodestringn -> fillern
     )
<Atom>
  <op>pred'</op>
  <slot>
    <Prop>
       <key><Const type="rif:iri">cpt:price</Const></key> <val><Const type="xsd:integer">49</Const></val><key><Name>unicodestring1</Name></key>
      <val>filler1'</val>
    </Prop>
  </slot>
   . . .
  <slot>
    <Prop>
       <key><Const type="rif:iri">cpt:currency</Const></key> <val><Const type="rif:iri">curr:USD</Const></val><key><Name>unicodestringn</Name></key>
      <val>fillern'</val>
    </Prop>
  </slot>
 </Frame> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And> 5.2 XML for RIF-BLD Rule Language We now extend the RIF-BLD serialization from Section XML for RIF-BLD Condition Language by including rules as described in Section EBNF for RIF-BLD Rule Language</Atom>
func (
  unicodestring1 -> filler1
  .  The extended serialization uses the following additional tags. - Group (nested collection of rules annotated with metadata) - meta (meta role, containing metadata, which is represented as a Frame) - rule (rule role, containing RULE) - Forall (quantified formula for 'Forall', containing declare and formula roles) - Implies (implication, containing if and then roles) - if (antecedent role, containing FORMULA) - then (consequent role, containing ATOMIC) The XML Schema Definition of RIF-BLD is given in Appendix XML Schema for BLD.  Example 6 (Serializing a RIF-BLD group annotated with metadata). This example shows a serialization for the group from Example 3. For convenience, the group is reproduced at the top and then is followed by its serialization. Compact URI prefixes: bks expands into http://example.com/books# auth expands into http://example.com/authors# cpt expands into http://example.com/concepts# dc expands into http://dublincore.org/documents/dces/ w3 expands into http://www.w3.org/ Presentation syntax: Group " http://sample.org "^^rif:iri["dc:publisher"^^rif:iri->"w3:W3C"^^rif:iri "dc:date"^^rif:iri->"2008-04-04"^^xsd:date] ( Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays ( "cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item) :- And("cpt:perishable"^^rif:iri(?item) "cpt:delivered"^^rif:iri(?item ?deliverydate "ppl:John"^^rif:iri) "cpt:scheduled"^^rif:iri(?item ?scheduledate) External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration)) External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffduration ?diffdays)) External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer))) ) Forall ?item ( "cpt:reject"^^rif:iri("ppl:Fred"^^rif:iri ?item) :- "cpt:unsolicited"^^rif:iri(?item) ).
  unicodestringn -> fillern
     )
 XML syntax: <Group> <meta><Expr>
  <op>func'</op>
  <slot>
    <Prop>
      <key><Name>unicodestring1</Name></key>
      <val>filler1'</val>
    </Prop>
  </slot>
   . . .
  <slot>
    <Prop>
      <key><Name>unicodestringn</Name></key>
      <val>fillern'</val>
    </Prop>
  </slot>
</Expr>
inst [
  key1 -> filler1
  . . .
  keyn -> fillern
     ]
<Frame>
  <object> <Const type="rif:iri"> http://sample.org </Const>inst'</object>
  <slot>
    <Prop>
       <key><Const type="rif:iri">dc:publisher</Const></key> <val><Const type="rif:iri">w3:W3C</Const></val><key>key1'</key>
      <val>filler1'</val>
    </Prop>
  </slot>
   . . .
  <slot>
    <Prop>
       <key><Const type="rif:iri">dc:date</Const></key> <val><Const type="xsd:date">2008-04-04</Const></val><key>keyn'</key>
      <val>fillern'</val>
    </Prop>
  </slot>
</Frame>
 </meta> <rule> <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> <arg><Var>item</Var></arg> </Atom> </formula> <formula> <Atom> <op><Const type="rif:iri">cpt:delivered</Const></op> <arg><Var>item</Var></arg> <arg><Var>deliverydate</Var></arg> <arg><Const type="rif:iri">ppl:John</Const></arg> </Atom> </formula> <formula> <Atom> <op><Const type="rif:iri">cpt:scheduled</Const></op> <arg><Var>item</Var></arg> <arg><Var>scheduledate</Var></arg> </Atom> </formula> <formula> <External> <content> <Atom> <op><Const type="rif:iri">fn:subtract-dateTimes-yielding-dayTimeDuration</Const></op> <arg><Var>deliverydate</Var></arg> <arg><Var>scheduledate</Var></arg> <arg><Var>diffduration</Var></arg> </Atom> </content> </External> </formula> <formula> <External> <content> <Atom> <op><Const type="rif:iri">fn:get-days-from-dayTimeDuration</Const></op> <arg><Var>diffduration</Var></arg> <arg><Var>diffdays</Var></arg> </Atom> </content> </External> </formula> <formula> <External> <content> <Atom> <op><Const type="rif:iri">op:numeric-greater-than</Const></op> <arg><Var>diffdays</Var></arg> <arg><Const type="xsd:long">10</Const></arg> </Atom> </content> </External> </formula> </And> </if> <then> <Atom> <op><Const type="xsd:long">reject</Const></op> <arg><Const type="rif:iri">ppl:John</Const></arg> <arg><Var>item</Var></arg> </Atom> </then> </Implies> </formula> </Forall> </rule> <rule> <Forall> <declare><Var>item</Var></declare> <formula> <Implies> <if> <Atom> <op><Const type="rif:iri">cpt:unsolicited</Const></op> <arg><Var>item</Var></arg> </Atom> </if> <then> <Atom> <op><Const type="rif:iri">cpt:reject</Const></op> <arg><Const type="rif:iri">ppl:Fred</Const></arg> <arg><Var>item</Var></arg> </Atom> </then> </Implies> </formula> </Forall> </rule> </Group> 5.3 Translation Between the RIF-BLD Presentation and XML Syntaxes We now show how to translate between the presentation and XML syntaxes of RIF-BLD. 5.3.1inst # class [
  key1 -> filler1
  . . .
  keyn -> fillern
             ]
<Frame>
  <object>
    <Member>
      <lower>inst'</lower>
      <upper>class'</upper>
    </Member>
  </object>
  <slot>
    <Prop>
      <key>key1'</key>
      <val>filler1'</val>
    </Prop>
  </slot>
   . . .
  <slot>
    <Prop>
      <key>keyn'</key>
      <val>fillern'</val>
    </Prop>
  </slot>
</Frame>
sub ## super [
  key1 -> filler1
  . . .
  keyn -> fillern
             ]
<Frame>
  <object>
    <Subclass>
      <lower>sub'</lower>
      <upper>super'</upper>
    </Subclass>
  </object>
  <slot>
    <Prop>
      <key>key1'</key>
      <val>filler1'</val>
    </Prop>
  </slot>
   . . .
  <slot>
    <Prop>
      <key>keyn'</key>
      <val>fillern'</val>
    </Prop>
  </slot>
</Frame>
inst # class
<Member>
  <lower>inst'</lower>
  <upper>class'</upper>
</Member>
sub ## super
<Subclass>
  <lower>sub'</lower>
  <upper>super'</upper>
</Subclass>
left = right
<Equal>
  <side>left'</side>
  <side>right'</side>
</Equal>
unicodestring^^space
<Const type="space">unicodestring</Const>
?unicodestring
<Var>unicodestring</Var>

4.3.2 Translation of the RIF-BLD ConditionRule Language

The translation between the presentation syntax and the XML syntax of the RIF-BLD ConditionRule Language is specifiedgiven by the table below. Since the presentation syntax of RIF-BLD is context sensitive,below, which extends the translation must differentiate between the terms that occur in the positiontable of the individuals from terms that occur as atomic formulas. To this end, in theSection 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 expressionsof the form func (...). The prime symbol (for instance, variable ' ) indicates that the translation function defined by the table must be applied recursively (i.e., to variable in our example).RIF-BLD Condition Language.


Presentation Syntax XML Syntax
 AndGroup (
   conjunctclause1
   . . .
   conjunctclausen
      )
 <And> <formula> conjunct<Group>
  <sentence>clause1' </formula></sentence>
   . . .
   <formula> conjunct<sentence>clausen' </formula> </And> Or</sentence>
</Group>
Group metaframe (
                   disjunctclause1
                   . . .
                   disjunctclausen
                )
 <Or> <formula> disjunct<Group>
  <meta>metaframe'</meta>
  <sentence>clause1' </formula></sentence>
   . . .
   <formula> disjunct<sentence>clausen' </formula> </Or> Exists</sentence>
</Group>
Forall
  variable1
   . . .
  variablen (
              bodyrule
            )
 <Exists><Forall>
  <declare>variable1'</declare>
   . . .
  <declare>variablen'</declare>
  <formula> body'rule'</formula>
 </Exists> pred ( argument 1 . . . argument n ) <Atom> <op> pred' </op> <arg> argument 1 ' </arg> . . . <arg> argument n ' </arg> </Atom> External ( atomexpr ) <External> <content> atomexpr' </content> </External> func ( argument 1 . . . argument n ) <Expr> <op> func' </op> <arg> argument 1 ' </arg> . . . <arg> argument n ' </arg> </Expr> pred ( unicode 1 -> filler 1 . .</Forall>
conclusion :- condition
<Implies>
  <if>condition'</if>
  <then>conclusion'</then>
</Implies>


5 RIF-BLD as a Specialization of the RIF Framework

This normative section describes RIF-BLD by specializing RIF-FLD. The reader is assumed to be familiar with RIF-FLD as described in RIF Framework for Logic-Based Dialects. unicode n -> filler n ) <Atom> <op> pred' </op> <slot> <Prop> <key><Name> unicode 1 </Name></key> <val> filler 1 ' </val> </Prop> </slot>The reader who is not interested in how RIF-BLD is derived from the framework can skip this section.


5.1 The Syntax of RIF-BLD as a Specialization of RIF-FLD

This section defines the precise relationship between the syntax of RIF-BLD and the syntactic framework of RIF-FLD.

The syntax of the RIF Basic Logic Dialect is defined by specialization from the syntax of the RIF Syntactic Framework for Logic Dialects. Section Syntax of a RIF Dialect as a Specialization of the RIF Framework in that document lists the parameters of the syntactic framework, which we will now specialize for RIF-BLD.


  1. Alphabet.
  2. The alphabet of RIF-BLD is the alphabet of RIF-FLD with the negation symbols Neg and Naf excluded.
  3. Assignment of signatures to each constant symbol.
  4. <slot> <Prop> <key><Name> unicodeThe signature set of RIF-BLD contains the following signatures:

    1. Basic.
      • individual{ }
      • atomic{ }

      The signature individual{ } represents the context in which individual objects (but not atomic formulas) can appear.
      The signature atomic{ } represents the context where atomic formulas can occur.

    2. For every integer n </Name></key> <val> filler 0, there are signatures
      • fn ' </val> </Prop> </slot> </Atom> func ( unicode 1 -> filler 1 . . . unicode{(individual ... individual) individual} -- for n-ary function symbols,
      • pn -> filler{(individual ... individual) atomic} -- for n-ary predicates.

      These represent function and predicate symbols of arity n ) <Expr> <op> func' </op> <slot> <Prop> <key><Name> unicode 1 </Name></key> <val> filler 1 ' </val> </Prop> </slot> . . . <slot> <Prop> <key><Name> unicode(each of the above cases has n </Name></key> <val> fillerindividuals as arguments inside the parentheses).

    3. For every set of symbols s1,...,sk SigNames, there are signatures fs1...sk{(s1->individual ... sk->individual) individual} and ps1...sk{(s1->individual ... sk->individual) atomic}. These are signatures for terms with named arguments and predicates with arguments named s1, ..., sk, respectively. Unlike in RIF-FLD, the argument names s1, ..., sk must be pairwise distinct.
    4. A symbol in Const can have exactly one signature, individual, fn ' </val> </Prop> </slot> </Expr> inst [ key 1 -> filler 1 . . . key, or pn -> filler, where n ] <Frame> <object> inst' </object> <slot> <Prop> <key> key 1 ' </key> <val> filler 1 ' </val> </Prop> </slot> . . 0, or fs1...sk{(s1->individual ... sk->individual) individual}, ps1...sk{(s1->individual ... sk->individual) atomic}, for some s1,...,sk SigNames. <slot> <Prop> <key> keyIt cannot have the signature atomic, since only complex terms can have such signatures. Thus, by itself a symbol cannot be a proposition in RIF-BLD, but a term of the form p() can be.

      Thus, in RIF-BLD each constant symbol can be either an individual, a predicate of one particular arity or with certain argument names, an externally defined predicate of one particular arity, or an externally defined function symbol of one particular arity -- it is not possible for the same symbol to play more than one role.

    5. The constant symbols that belong to the supported RIF data types (XML Schema data types, rdf:XMLLiteral, rif:text) all have the signature individual in RIF-BLD.
    6. The symbols of type rif:iri and rif:local can have the following signatures in RIF-BLD: individual, fn ' </key> <val> filler, or pn ' </val> </Prop> </slot> </Frame> inst # class [ key 1 -> filler 1, for n = 0,1,....; or fs1...sk, ps1...sk, for some argument names s1,...,sk SigNames.
    7. All variables are associated with signature individual{ }, so they can range only over individuals.
    8. The signature for equality is ={(individual individual) atomic}.

      This means that equality can compare only those terms whose signature is individual; it cannot compare predicate names or function symbols. Equality terms are also not allowed to occur inside other terms, since the above signature implies that any term of the form t = s has signature atomic and not individual.

    9. key nThe frame signature, -> filler n ] <Frame> <object> <Member> <lower> inst' </lower> <upper> class' </upper> </Member> </object> <slot> <Prop> <key> key 1 ' </key> <val> filler 1 ' </val> </Prop> </slot> ., is ->{(individual individual individual) atomic}.

      Note that this precludes the possibility that a frame term might occur as an argument to a predicate, a function, or inside some other term.

    10. The membership signature, #, is #{(individual individual) atomic}.

      <slot> <Prop> <key> key n ' </key> <val> filler n ' </val> </Prop> </slot> </Frame> sub ## super [ key 1 -> filler 1Note that this precludes the possibility that a membership term might occur as an argument to a predicate, a function, or inside some other term.

    11. The signature for the subclass relationship is ##{(individual individual) atomic}.

      As with frames and membership terms, this precludes the possibility that a subclass term might occur inside some other term.

    RIF-BLD uses no special syntax for declaring signatures. Instead, the author specifies signatures contextually. That is, since RIF-BLD requires that each symbol is associated with a unique signature, the signature is determined from the context in which the symbol is used. If a symbol is used in more than one context, the parser must treat this as a syntax error. If no errors are found, all terms and atomic formulas are guaranteed to be well-formed. Thus, signatures are not part of the RIF-BLD language, and individual and atomic are not reserved keywords in RIF-BLD.

  5. Supported types of terms.
    • key n -> filler n ] <Frame> <object> <Subclass> <lower> sub' </lower> <upper> super' </upper> </Subclass> </object> <slot> <Prop> <key> key 1 ' </key> <val> filler 1 ' </val> </Prop> </slot>RIF-BLD supports all the term types defined by the syntactic framework (see Well-formed Terms and Formulas):
      1. constants
      2. variables
      3. positional
      4. with named arguments
      5. equality
      6. frame
      7. membership
      8. subclass
      9. external
    • Compared to RIF-FLD, terms (both positional and with named arguments) have significant restrictions. This is so in order to give BLD a relatively compact nature.
      • The signature for the variable symbols does not permit them to occur in the context of predicates, functions, or formulas. In particular, unlike in RIF-FLD, a variable is not an atomic formula in RIF-BLD.
      • Likewise, a symbol cannot be an atomic formula by itself. That is, if p Const then p is not a well-formed atomic formula. However, p() can be an atomic formula.
      • Signatures permit only constant symbols to occur in the context of function or predicate names. Indeed, RIF-BLD signatures ensure that all variables have the signature individual{ } and all other terms, except for the constants from Const, can have either the signature individual{ } or atomic{ }. Therefore, if t is a (non-Const) term then t(...) is not a well-formed term.
  6. Supported symbol spaces.
  7. RIF-BLD supports all the symbol spaces defined in Section Symbol Spaces of the syntactic framework:

    • xsd:string
    • xsd:decimal
    • xsd:time
    • xsd:date
    • xsd:dateTime
    • rdf:XMLLiteral
    • rif:text
    • rif:iri
    • rif:local
  8. Supported formulas.
  9. <slot> <Prop> <key> key n ' </key> <val> filler n ' </val> </Prop> </slot> </Frame> inst # class <Member> <lower> inst' </lower> <upper> class' </upper> </Member> sub ## super <Subclass> <lower> sub' </lower> <upper> super' </upper> </Subclass> left = right <Equal> <side> left' </side> <side> right' </side> </Equal> unicode ^^ space <Const type=" space "> unicode </Const> ? unicode <Var> unicode </Var> 5.3.2 TranslationRIF-BLD supports the following types of formulas (see Well-formed Terms and Formulas for the definitions):

    • RIF-BLD condition
    • A RIF-BLD condition is a conjunctive and disjunctive combination of atomic formulas with optional existential quantification of variables.

    • RIF-BLD rule
    • A RIF-BLD rule is a universally quantified RIF-FLD rule with the following restrictions:

      • The head (or conclusion) of the rule is an atomic formula, which is not an externally defined predicate (i.e., it cannot have the form External(...)).
      • The body (or premise) of the rule is a RIF-BLD condition.
      • All free (non-quantified) variables in the rule must be quantified with Forall outside of the rule (i.e., Forall ?vars (head :- body)).
    • RIF-BLD group

      A RIF-BLD group is a RIF-FLD group that contains only RIF-BLD rules and RIF-BLD groups.

Recall that negation (classical or default) is not supported by RIF-BLD in either the rule Languagehead or the translationbody.

The list of supported symbol spaces will move to another document, Data Types and Built-Ins. Any existing discrepancies will be fixed at that time.


5.2 The Semantics of RIF-BLD as a Specialization of RIF-FLD

This normative section defines the precise relationship between the presentationsemantics of RIF-BLD and the semantic framework of RIF-FLD. Specification of the semantics that does not rely on RIF-FLD is given in Section Direct Specification of RIF-BLD Semantics.

The semantics of the RIF Basic Logic Dialect is defined by specialization from the semantics of the Semantic Framework for Logic Dialects of RIF. Section Semantics of a RIF Dialect as a Specialization of the RIF Framework in that document lists the parameters of the semantic framework, which we need to specialize for RIF-BLD.

Recall that the semantics of a dialect is derived from these notions by specializing the following parameters.

  • The effect of the syntax.
  • RIF-BLD does not support negation. This is the only obvious simplification with respect to RIF-FLD as far as the semantics is concerned.

  • Truth values.
  • The set TV of truth values in RIF-BLD consists of just two values, t and f such that f <t t. Clearly, <t is a total order here.

  • Data types.
  • RIF-BLD supports all the data types listed in Section Primitive Data Types of RIF-FLD:

    • xsd:long
    • xsd:integer
    • xsd:decimal
    • xsd:string
    • xsd:time
    • xsd:dateTime
    • rdf:XMLLiteral
    • rif:text
  • Logical entailment.
  • Recall that logical entailment in RIF-FLD is defined with respect to an unspecified set of intended semantic structures and the XML syntaxthat dialects of the RIF-BLD Rule LanguageRIF must make this notion concrete. For RIF-BLD, this set is given bydefined in one of the table below, which extendstwo following equivalent ways:

    • as a set of all models; or
    • as the translation tableunique minimal model.

    These two definitions are equivalent for entailment of Section TranslationRIF-BLD conditions by RIF-BLD sets of formulas, since all rules in RIF-BLD Condition Language . Presentation Syntax XML Syntax Group ( clause 1 . . . clause n ) <Group> <rule> clause 1 ' </rule> . . . <rule> clause n ' </rule> </Group> Group metaframe ( clause 1 . . . clause n ) <Group> <meta> metaframe' </meta> <rule> clause 1 ' </rule> . . . <rule> clause n ' </rule> </Group> Forall variable 1 . . . variable n ( rule ) <Forall> <declare> variable 1 ' </declare> . .are Horn -- it is a classical result of Van Emden and Kowalski [vEK76].

The list of supported data types will move to another document, Data Types and Built-Ins. <declare> variable n ' </declare> <formula> rule' </formula> </Forall> conclusion :- condition <Implies> <if> condition' </if> <then> conclusion' </then> </Implies>Any existing discrepancies will be fixed at that time.


6 References

6.1 Normative References

[RDF-CONCEPTS]
Resource Description Framework (RDF): Concepts and Abstract Syntax, Klyne G., Carroll J. (Editors), W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/. Latest version available at http://www.w3.org/TR/rdf-concepts/.

[RDF-SEMANTICS]
RDF Semantics, Patrick Hayes, Editor, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-mt-20040210/. Latest version available at http://www.w3.org/TR/rdf-mt/.

[RDF-SCHEMA]
RDF Vocabulary Description Language 1.0: RDF Schema, Brian McBride, Editor, W3C Recommendation 10 February 2004, http://www.w3.org/TR/rdf-schema/.

[RFC-3066]
RFC 3066 - Tags for the Identification of Languages, H. Alvestrand, IETF, January 2001. This document is http://www.isi.edu/in-notes/rfc3066.txt.

[RFC-3987]
RFC 3987 - Internationalized Resource Identifiers (IRIs), M. Duerst and M. Suignard, IETF, January 2005. This document is http://www.ietf.org/rfc/rfc3987.txt.

[XML-SCHEMA2]
XML Schema Part 2: Datatypes, W3C Recommendation, World Wide Web Consortium, 2 May 2001. This version is http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/. The latest version is available at http://www.w3.org/TR/xmlschema-2/.

6.2 Informational References

[ANF01]
Normal Form Conventions for XML Representations of Structured Data, Henry S. Thompson. October 2001.

[KLW95]
Logical foundations of object-oriented and frame-based languages, M. Kifer, G. Lausen, J. Wu. Journal of ACM, July 1995, pp. 741--843.

[CKW93]
HiLog: A Foundation for higher-order logic programming, W. Chen, M. Kifer, D.S. Warren. Journal of Logic Programming, vol. 15, no. 3, February 1993, pp. 187--230.

[CK95]
Sorted HiLog: Sorts in Higher-Order Logic Data Languages, W. Chen, M. Kifer. Sixth Intl. Conference on Database Theory, Prague, Czech Republic, January 1995, Lecture Notes in Computer Science 893, Springer Verlag, pp. 252--265.

[RDFSYN04]
RDF/XML Syntax Specification (Revised), Dave Beckett, Editor, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-syntax-grammar-20040210/. Latest version available at http://www.w3.org/TR/rdf-syntax-grammar/.

[Shoham87]
Nonmonotonic logics: meaning and utility, Y. Shoham. Proc. 10th International Joint Conference on Artificial Intelligence, Morgan Kaufmann, pp. 388--393, 1987.

[CURIE]
CURIE Syntax 1.0: A compact syntax for expressing URIs, Mark Birbeck. Draft, 2005. Available at http://www.w3.org/2001/sw/BestPractices/HTML/2005-10-27-CURIE.

[CycL]
The Syntax of CycL, Web site. Available at http://www.cyc.com/cycdoc/ref/cycl-syntax.html.

[FL2]
FLORA-2: An Object-Oriented Knowledge Base Language, M. Kifer. Web site. Available at http://flora.sourceforge.net.

[OOjD]
Object-Oriented jDREW, Web site. Available at http://www.jdrew.org/oojdrew/.

[GRS91]
The Well-Founded Semantics for General Logic Programs, A. Van Gelder, K.A. Ross, J.S. Schlipf. Journal of ACM, 38:3, pages 620-650, 1991.

[GL88]
The Stable Model Semantics for Logic Programming, M. Gelfond and V. Lifschitz. Logic Programming: Proceedings of the Fifth Conference and Symposium, pages 1070-1080, 1988.

[vEK76]
The semantics of predicate logic as a programming language, M. van Emden and R. Kowalski. Journal of the ACM 23 (1976), 733-742.


7 Appendix: Subdialects of RIF-BLD

The following is a proposal, under discussion, for specifying RIF-CORE and some other subdialects of BLD by removing certain syntactic constructs from RIF-BLD and the corresponding restrictions on the semantics (hence, by further specializing RIF-BLD). For some engines it might be preferable or more natural to support only some subdialects of RIF-BLD. These subdialects of BLD can also be reused in the definitions of other RIF dialects.

The syntactic structure of RIF-BLD suggests several useful subdialects:

  • RIF-CORE. This subdialect is obtained from RIF-BLD by removing support for:
    • equality formulas in the rule conclusions (while still allowing them in conditions)
    • terms with named arguments
    • membership, subclass, and frame terms
  • RIF-CORE+equality.
    • This subdialect extends RIF-CORE by adding support for equality formulas in the rule conclusions.
  • RIF-CORE+named arguments.
    • This subdialect extends RIF-CORE by adding syntactic support for terms with named arguments.


8 Appendix: XML Schema for RIF-BLD

The namespace of RIF is http://www.w3.org/2007/rif#.

XML schemas for the RIF-BLD sublanguages are available below and online, with examples.


8.1 Condition Language

<?xml version="1.0" encoding="UTF-8"?>

<xs:schema 
 xmlns:xs="http://www.w3.org/2001/XMLSchema"
 xmlns="http://www.w3.org/2007/rif#"
 targetNamespace="http://www.w3.org/2007/rif#"
 elementFormDefault="qualified"
 version="Id: BLDCond.xsd,v 0.8  2008-04-072008-04-09 dhirtle/hboley">

 <xs:annotation>
   <xs:documentation>
   This is the XML schema for the Condition Language as defined by
   Working Draft 2 of the RIF Basic Logic Dialect.
   
   The schema is based on the following EBNF for the RIF-BLD Condition Language:

 FORMULA        ::= 'And' '(' FORMULA* ')' |
                    'Or' '(' FORMULA* ')' |
                    'Exists' Var+ '(' FORMULA ')' |
                    ATOMIC |
                    'External' '(' Atom ')'
 ATOMIC         ::= Atom | Equal | Member | Subclass | Frame
 Atom           ::= UNITERM
 UNITERM        ::= Const '(' (TERM* | (Name '->' TERM)*) ')'
 Equal          ::= TERM '=' TERM
 Member         ::= TERM '#' TERM
 Subclass       ::= TERM '##' TERM
 Frame          ::= TERM '[' (TERM '->' TERM)* ']'
 TERM           ::= Const | Var | Expr | 'External' '(' Expr ')'
 Expr           ::= UNITERM
 Const          ::= '"' UNICODESTRING '"^^' SYMSPACE
 Name           ::= UNICODESTRING
 Var            ::= '?' UNICODESTRING

   </xs:documentation>
 </xs:annotation>
 
 <xs:group name="FORMULA">  
   <xs:choice>
     <xs:element ref="And"/>
     <xs:element ref="Or"/>
     <xs:element ref="Exists"/>
     <xs:group ref="ATOMIC"/>
     <xs:element name="External" type="External-FORMULA.type"/>
   </xs:choice>
 </xs:group>
 
 <xs:complexType name="External-FORMULA.type">
   <xs:sequence>
     <xs:element name="content" type="content-FORMULA.type"/>
   </xs:sequence>
 </xs:complexType>
 
 <xs:complexType name="content-FORMULA.type">
   <xs:sequence>
     <xs:element ref="Atom"/>
   </xs:sequence>
 </xs:complexType>

 <xs:element name="And">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="formula" minOccurs="0" maxOccurs="unbounded"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="Or">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="formula" minOccurs="0" maxOccurs="unbounded"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="Exists">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="declare" minOccurs="1" maxOccurs="unbounded"/>
       <xs:element ref="formula"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="formula">
   <xs:complexType>
     <xs:sequence>
       <xs:group ref="FORMULA"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="declare">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="Var"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>

 <xs:group name="ATOMIC">
   <xs:choice>
     <xs:element ref="Atom"/>
     <xs:element ref="Equal"/>
     <xs:element ref="Member"/>
     <xs:element ref="Subclass"/>
     <xs:element ref="Frame"/>
   </xs:choice>
 </xs:group>
 
 <xs:element name="Atom">
   <xs:complexType>
     <xs:sequence>
       <xs:group ref="UNITERM"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>  
 
 <xs:group name="UNITERM">
   <xs:sequence>
     <xs:element ref="op"/>
     <xs:choice>
       <xs:element ref="arg" minOccurs="0" maxOccurs="unbounded"/>
       <xs:element  ref="slot"name="slot" type="slot-UNITERM.type" minOccurs="0" maxOccurs="unbounded"/>
     </xs:choice>
   </xs:sequence>
 </xs:group>

 <xs:element name="op">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="Const"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="arg">
   <xs:complexType>
     <xs:sequence>
       <xs:group ref="TERM"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>

  <xs:element name="slot"> <xs:complexType><xs:complexType name="slot-UNITERM.type">
   <xs:sequence>
     <xs:element  ref="Prop"/>name="Prop" type="Prop-UNITERM.type"/>
   </xs:sequence>
 </xs:complexType>

  </xs:element> <xs:element name="Prop"> <xs:complexType><xs:complexType name="Prop-UNITERM.type">
   <xs:sequence>
     <xs:element  ref="key"/>name="key" type="key-UNITERM.type"/>
     <xs:element ref="val"/>
   </xs:sequence>
 </xs:complexType>

  </xs:element> <xs:element name="key"> <xs:complexType> <xs:choice><xs:complexType name="key-UNITERM.type">
   <xs:sequence>
     <xs:element ref="Name"/>
    <xs:group ref="TERM"/> </xs:choice></xs:sequence>
 </xs:complexType>

  </xs:element><xs:element name="val">
   <xs:complexType>
     <xs:sequence>
       <xs:group ref="TERM"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>

 <xs:element name="Equal">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="side"/>
       <xs:element ref="side"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="side">
   <xs:complexType>
     <xs:sequence>
       <xs:group ref="TERM"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="Member">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="lower"/>
       <xs:element ref="upper"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>

 <xs:element name="Subclass">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="lower"/>
       <xs:element ref="upper"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="lower">
   <xs:complexType>
     <xs:sequence>
       <xs:group ref="TERM"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="upper">
   <xs:complexType>
     <xs:sequence>
       <xs:group ref="TERM"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="Frame">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="object"/>
       <xs:element  ref="slot"name="slot" type="slot-Frame.type" minOccurs="0" maxOccurs="unbounded"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>

 <xs:element name="object">
   <xs:complexType>
     <xs:choice>
       <xs:group ref="TERM"/>
       <xs:element ref="Member"/>
       <xs:element name="Subclass"/>
     </xs:choice>
   </xs:complexType>
 </xs:element>

 <xs:complexType name="slot-Frame.type">
   <xs:sequence>
     <xs:element name="Prop" type="Prop-Frame.type"/>
   </xs:sequence>
 </xs:complexType>

 <xs:complexType name="Prop-Frame.type">
   <xs:sequence>
     <xs:element name="key" type="key-Frame.type"/>
     <xs:element ref="val"/>
   </xs:sequence>
 </xs:complexType>
 
 <xs:complexType name="key-Frame.type">
   <xs:sequence>
     <xs:group ref="TERM"/>
   </xs:sequence>
 </xs:complexType>

 <xs:group name="TERM">  
     <xs:choice>
        <xs:element ref="Const"/>
        <xs:element ref="Var"/>
        <xs:element ref="Expr"/>
        <xs:element name="External" type="External-TERM.type"/>
     </xs:choice>
 </xs:group>
 
 <xs:complexType name="External-TERM.type">
   <xs:sequence>
     <xs:element name="content" type="content-TERM.type"/>
   </xs:sequence>
 </xs:complexType>
 
 <xs:complexType name="content-TERM.type">
   <xs:sequence>
     <xs:element ref="Expr"/>
   </xs:sequence>
 </xs:complexType>

 <xs:element name="Expr">
   <xs:complexType>
     <xs:sequence>
       <xs:group ref="UNITERM"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>

 <xs:element name="Const">
   <xs:complexType mixed="true">
     <xs:sequence/>
     <xs:attribute name="type" type="xs:string" use="required"/>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="Name" type="xs:string">
 </xs:element>

 <xs:element name="Var" type="xs:string">
 </xs:element>
 
</xs:schema>

8.2 Rule Language

<?xml version="1.0" encoding="UTF-8"?>

<xs:schema 
 xmlns:xs="http://www.w3.org/2001/XMLSchema"
 xmlns="http://www.w3.org/2007/rif#"
 targetNamespace="http://www.w3.org/2007/rif#"
 elementFormDefault="qualified"
 version="Id: BLDRule.xsd,v 0.8  2008-04-072008-04-09 dhirtle/hboley">

 <xs:annotation>
   <xs:documentation>
   This is the XML schema for the Rule Language as defined by
   Working Draft 2 of the RIF Basic Logic Dialect.
   
   The schema is based on the following EBNF for the RIF-BLD Rule Language:
 
 Document ::= Group
 Group    ::= 'Group' IRIMETA? '(' (RULE | Group)* ')'
 IRIMETA  ::= Frame
 RULE     ::= 'Forall' Var+ '(' CLAUSE ')' | CLAUSE
 CLAUSE   ::= Implies | ATOMIC
 Implies  ::= ATOMIC ':-' FORMULA
   
   Note that this is an extension of the syntax for the RIF-BLD Condition Language (BLDCond.xsd).
   </xs:documentation>
 </xs:annotation>

 <xs:include schemaLocation="BLDCond.xsd"/>

 <xs:element name="Document">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="Group"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="Group">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="meta" minOccurs="0" maxOccurs="1"/>
        <xs:sequence> <xs:choice minOccurs="0" maxOccurs="unbounded"> <xs:element ref="rule"/><xs:element  ref="Group"/> </xs:choice> </xs:sequence>ref="sentence" minOccurs="0" maxOccurs="unbounded"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>

 <xs:element name="meta">
   <xs:complexType>
     <xs:sequence>
       <xs:group ref="IRIMETA"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>

 <xs:group name="IRIMETA">
   <xs:sequence>
     <xs:element ref="Frame"/>
   </xs:sequence>
 </xs:group>

 <xs:element  name="rule">name="sentence">
  <xs:complexType>
     <xs:sequence><xs:choice>
      <xs:element ref="Group"/>
      <xs:group ref="RULE"/>
     </xs:sequence></xs:choice>
  </xs:complexType>
</xs:element>
 
 <xs:group name="RULE">
   <xs:choice>
     <xs:element ref="Forall"/>
     <xs:group ref="CLAUSE"/>
   </xs:choice>
 </xs:group>

 <xs:element name="Forall">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="declare" minOccurs="1" maxOccurs="unbounded"/>
       <xs:element name="formula">
         <xs:complexType>
           <xs:group ref="CLAUSE"/>
         </xs:complexType>
       </xs:element>
     </xs:sequence>
   </xs:complexType>
 </xs:element>

 <xs:group name="CLAUSE">  
   <xs:choice>
     <xs:element ref="Implies"/>
     <xs:group ref="ATOMIC"/>
   </xs:choice>
 </xs:group>
 
 <xs:element name="Implies">
   <xs:complexType>
     <xs:sequence>
       <xs:element ref="if"/>
       <xs:element ref="then"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>

 <xs:element name="if">
   <xs:complexType>
     <xs:sequence>
       <xs:group ref="FORMULA"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
 <xs:element name="then">
   <xs:complexType>
     <xs:sequence>
       <xs:group ref="ATOMIC"/>
     </xs:sequence>
   </xs:complexType>
 </xs:element>
 
</xs:schema>