Copyright © 2008 W3C® (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark and document use rules apply.
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.
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:
This draft is ready for Working Group Review. A publication decision is scheduled for 15 April.
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.
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.
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.
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 lá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:
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.
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.
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.
Definition
(Alphabet). Section SyntaxThe alphabet of RIF-BLD consists
of
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 |
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.
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).
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.
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.
. 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
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.
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 |
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:
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.
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).
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 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)) TermsofRIF-FLD.Also,ifatermofwith 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])
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 ::= FrametermsarealsoRULE ::= 'Forall' Var+ '(' CLAUSE ')' | CLAUSE CLAUSE ::= Implies | ATOMICformulas.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.
FORMULAisanatomic::= 'And' '(' FORMULA* ')' | 'Or' '(' FORMULA* ')' | 'Exists' Var+ '(' FORMULAthat')' | 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:
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))) )andGroup(ρ1...ρnb. Universal-existential form: Forall ?item ( "cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item )aregroupformulas.:- 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) ) )
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.
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.
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:
This mapping interprets constant symbols. In addition:
This mapping interprets variable symbols.
This mapping interprets positional terms. In addition:
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:
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.
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.
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.
It gives meaning to the presentation syntaxequality operator.
It is used to define truth valuation for Horn rules extendsformulas.
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:
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:
Here D iswe use {...} to denote a non-emptyset of elements called the domainargument/value pairs.
Here {...} denotes a bag of attribute/value pairs.
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:
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 ☐
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:
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:
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:
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:
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.
The empty conjunction is treated as a tautology, so
TValI truth(And()) = t.
The expected properties, itempty disjunction is required that:treated as a contradiction, so
TValI truth(Or()) = f.
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.
If Γ is a group formula of the form Group φ (ρ1 ... ρn) or Group (ρ1 ... ρn) then
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.
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 ☐
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.
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) - Externalschemas,tcanbe(external call, containing a content role) - content (content role, containing aninstanceofatmostonesuchschema,soI(External(t))iswell-defined.Conjunction:TValI(And(c1...cn))=tifAtom, 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 andonlyifTValI(c1)=...=TValI(cn)=t.Otherwise,TValI(And(c1...cn))=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 AndonlyifforeveryI*,describedbelow,TValI*(φ(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.HereI*isasemanticstructureXML 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>
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 ofrulessentences annotated with metadata) - meta (meta role, containing metadata, which istreatedrepresented as aconjunction.ThemetadataisignoredFrame) - sentence (sentence role, containing RULE or Group) - Forall (quantified formula forpurposesof'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,wecansaythatΓ |= φholdsiffwheneverI|=ΓitfollowsthatalsoI|= φ.☐5XMLSerializationSyntaxforRIF-BLDTheXMLserializationforRIF-BLDisalternatingorfullystriped[ANF01].AfullystripedserializationviewsXMLdocumentsasobjectsanddividesallXMLtagsintoclassdescriptors,calledtypetags,andpropertydescriptors,calledroletags.Weusecapitalizednamesfortypetagsandlowercasenamesforroletags.5.1XMLforRIF-BLDConditionLanguageXMLserializationofthepresentationsyntaxofSectionEBNFforRIF-BLDConditionLanguageusesthefollowingtags.-And(conjunction)-Or(disjunction)-Exists(quantifiedformulafor'Exists',containingdeclareandformularoles)-declare(declarerole,containingaVar)-formula(formularole,containingaFORMULA)-Atom(atomformula,positionalorwithnamedarguments)-External(externalcall,containingacontentrole)-content(contentrole,containinganAtom,forpredicates,orExpr,forfunctions)-Member(memberformula)-Subclass(subclassformula)-Frame(Frameformula)-object(Member/Framerole,containingaTERMoranobjectdescription)-op(Atom/Exprroleforpredicates/functionsasoperations)-arg(positionalargumentrole)-upper(Member/Subclassupperclassrole)-lower(Member/Subclasslowerinstance/classrole)-slot(Atom/Expr/Frameslotrole,containingaProp)-Prop(Property,prefixversionofslotinfix'->')-key(Propkeyrole,containingaConst)-val(Propvalrole,containingaTERM)-Equal(prefixversionoftermequation'=')-Expr(expressionformula,positionalorwithnamedarguments)-side(Equalleft-handsidesyntax: <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>
We now show how to translate between the presentation and XML
Schema Definition (XSD)syntaxes of RIF-BLD.
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 |
---|---|
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> |
pred ( argument1 . . . argumentn ) |
<Atom> |
|
<External> <content>atomexpr'</content> </External> |
func ( argument1 . . . argumentn ) |
<Expr> |
|
<Atom> <op>pred'</op> <slot> <Prop> |
func ( unicodestring1 -> filler1 . |
|
inst [ key1 -> filler1 . . . keyn -> fillern ] |
<Frame> <object> |
|
<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> |
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 |
---|---|
|
|
Group metaframe ( |
|
Forall variable1 . . . variablen ( |
|
conclusion :- condition |
<Implies> <if>condition'</if> <then>conclusion'</then> </Implies> |
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.
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.
<slot> <Prop> <key><Name> unicodeThe signature set of RIF-BLD contains the following
signatures:
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.
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).
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.
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.
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.
<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.
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.
RIF-BLD supports all the symbol spaces defined in Section Symbol Spaces of the syntactic framework:
<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):
A RIF-BLD condition is a conjunctive and disjunctive combination of atomic formulas with optional existential quantification of variables.
A RIF-BLD rule is a universally quantified RIF-FLD rule with the following restrictions:
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. |
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.
RIF-BLD does not support negation. This is the only obvious simplification with respect to RIF-FLD as far as the semantics is concerned.
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.
RIF-BLD supports all the data types listed in Section Primitive Data Types of RIF-FLD:
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:
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. |
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:
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.
<?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.82008-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:elementref="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:elementname="slot"><xs:complexType><xs:complexType name="slot-UNITERM.type"> <xs:sequence> <xs:elementref="Prop"/>name="Prop" type="Prop-UNITERM.type"/> </xs:sequence> </xs:complexType></xs:element><xs:elementname="Prop"><xs:complexType><xs:complexType name="Prop-UNITERM.type"> <xs:sequence> <xs:elementref="key"/>name="key" type="key-UNITERM.type"/> <xs:element ref="val"/> </xs:sequence> </xs:complexType></xs:element><xs:elementname="key"><xs:complexType><xs:choice><xs:complexType name="key-UNITERM.type"> <xs:sequence> <xs:element ref="Name"/><xs:groupref="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:elementref="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>
<?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.82008-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:choiceminOccurs="0"maxOccurs="unbounded"><xs:elementref="rule"/><xs:elementref="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:elementname="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>