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.
The Appendix: List of Builtins is currently kept as an external link.
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/.
@@TBD
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 Format) based on a set of foundational concepts that are supposed to be shared by all logic-based RIF dialects.
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, internationalized resource identifiers (or IRIs, defined by RFC 3987 [RFC 3987]) as identifiers for concepts, and XML Schema data types. The last two features make RIF-BLD into a Web 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.
RIF-BLD is defined in two different ways. First, it is defined as a specialization of RIF-FLD, the RIF Framework for Logic-based Dialects; it is a very short description, but it requires familiarity with RIF-FLD. RIF-FLD provides a general framework -- both syntactic and semantic -- for defining RIF dialects. With this framework, one can extend RIF-BLD with default negation, higher-order features, and so on. Then RIF-BLD is described 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.
One fragment of RIF is called the Condition Language. It defines the syntax and semantics for the bodies of the rules in RIF-BLD. However, it is envisioned that this fragment will have a wider use in RIF. In particular, it will be used as queries, constraints, and in the conditional part in production rules (see RIF PRD), reactive rules, and normative rules.
The current document is the third 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 section defines the precise relationship between the syntax of RIF-BLD and the syntactic framework of RIF-FLD. The other sections describe RIF-BLD largely independently of RIF-FLD.
The syntax of the RIF Basic Logic Dialect is defined by specialization from the syntax of the Syntactic Framework for Logic Dialects of RIF. Section Syntax of a RIF Dialect as a Specialization of RIF-FLD in that document lists the parameters of the syntactic framework, which we will now specialize for RIF-BLD.
Alphabet.
The alphabet of RIF-BLD is the alphabet of RIF-FLD with the negation symbols neg and naf excluded
Assignment of signatures to each constant symbol.
term{ }, atomic{ }, bi_atomic{ }, where bi_atomic<atomic.
The signature term{ } represents the context in which individual objects (but not atomic formulas) can appear. The signature bi_atomic{ } represents atomic formulas for builtin predicates (such as fn:substring). Since bi_atomic<atomic, builtin atomic formulas are also atomic formulas, but normally most atomic formulas are user-defined and they will have the signature atomic rather than bi_atomic.
For every integer n ≥ 0, there are signatures f_{n}{(term ... term) ⇒ term}, p_{n}{(term ... term) ⇒ atomic}, and bi_{n}{(term ... term) ⇒ bi_atomic} (in each case there are n terms inside the parentheses). These represent function symbols of arity n, user-defined predicate symbols of arity n, and n-ary builtin predicates, respectively.
For every set of symbols s1,...,sk ∈ SigNames, there are signatures f_{s1...sk}{(s1->term ... sk->term) ⇒ term} and p_{s1...sk}{(s1->term ... sk->term) ⇒ atomic}. These are signatures for terms with named arguments and predicates with arguments named s1, ..., sk, respectively.
A symbol in Const can have exactly one signature, term, f_{n}, p_{n}, or bi_{n}, where n ≥ 0, or f_{s1...sk}{(s1->term ... sk->term) ⇒ term}, p_{s1...sk}{(s1->term ... sk->term) ⇒ atomic}, for some s1,...,sk ∈ SigNames. It cannot have the signature atomic or bi_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.
The constant symbols that correspond to XML Schema data types all have the signature term in RIF-BLD. The symbols of type rif:iri and rif:local can have the following signatures in RIF-BLD: term, f_{n}, p_{n}, or bi_{n}, for n = 0,1,....; or f_{s1...sk}, p_{s1...sk}, for some argument names s1,...,sk ∈ SigNames.
All variables are associated with signature term{ }, so they can range only over individuals.
The signature for equality is ={(term term) ⇒ atomic, (term term) ⇒ term}. This means that equality can compare only those terms whose signature is term; it cannot compare predicate names or function symbols.
The frame signature, ->, is ->{(term term term) ⇒ atomic, (term term term) ⇒ term}.
The membership signature, #, is #{(term term) ⇒ atomic, (term term) ⇒ term}.
The signature for the subclass relationship is ##{(term term) ⇒ atomic, (term term) ⇒ term}.
RIF-BLD uses no extra syntax for declaring signatures. Instead, signatures are inferred. Since RIF-BLD requires that each symbol is associated with a unique signature, the signature can be determined from the context in which the symbol is used. If a symbol is used in more than one context, the parser should treat it as a syntax error. If no errors are found, all terms and atomic formulas are guaranteed to be well-formed. As a consequence, signatures are not part of the RIF-BLD language and term, atomic, and bi_atomic are not reserved keywords in RIF-BLD.
Supported types of terms.
RIF-BLD supports all the term types defined by the syntactic framework (see Well-formed Terms and Formulas):
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 term{ } and all other terms, except for the constants from Const, can have either the signature term{ } or atomic{ }. Therefore, if t is a (non-Const) term then t(...) is not a well-formed term.
Supported symbol spaces.
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
Supported formulas.
RIF-BLD supports the following types of formulas (see Well-formed Terms and Formulas for the definitions):
RIF-BLD condition
RIF-BLD rule
The head (or conclusion) of the rule is an atomic formula, which is not a builtin predicate (i.e., its signature is atomic, but not bi_atomic).
The free variables in the rule can be optionally quantified with Forall outside of the rule (i.e., Forall ?vars (head :- body)).
In order to make this document self-contained, we will now define the syntax of RIF-BLD with no references to RIF-FLD -- except for Symbol Spaces whose definition we do not duplicate here.
The alphabet of RIF-BLD consists of a countably infinite set of constant symbols Const, a countably infinite set of variable symbols Var (disjoint from Const), a countably infinite set of argument names, ArgNames (disjoint from Const and Var), connective symbols And and Or, quantifiers Exists and Forall, the symbols =, #, ##, ->, :-, and auxiliary symbols, such as "(" and ")". The set of connective symbols, quantifiers, =, etc., is disjoint from Const and Var. Variables are written as Unicode strings preceded with the symbol "?". The syntax for constant symbols is given in Section Symbol Spaces of RIF-FLD.
The language of RIF-BLD is the set of formulas constructed using the above alphabet according to the rules spelled out below.
RIF-BLD supports several kinds of terms: constants and variables, positional terms, terms with named arguments, equality, membership, and subclass terms, and frames. The word "term" will be used to refer to any kind of terms. Formally, terms are defined as follows:
Constants and variables. If t ∈ Const or t ∈ Var then t is a simple term.
Positional terms. If t ∈ Const and t_{1}, ..., t_{n} are terms then t(t_{1} ... t_{n}) is a positional term.
Terms with named arguments. A term with named arguments (a term with named arguments) is of the form t(s_{1}->v_{1} ... s_{n}->v_{n}), where t ∈ Const, v_{1} , ..., v_{n} are terms (positional, with named arguments, frame, etc.), and s_{1}, ..., s_{n} are (not necessarily distinct) symbols from the set ArgNames. The term t here represents a predicate or a function; s_{1}, ..., s_{n} represent argument names; and v_{1} , ..., v_{n} represent argument values. Terms with named arguments are like positional terms except that the arguments are named and their order is immaterial. Note that a term like f() is both positional and with named arguments.
Equality terms. If t and s are terms then t = s is an equality term.
Class membership terms (or just membership terms). t#s is a membership term if t and s are arbitrary terms.
Subclass terms. t##s is a subclass term if t and s are arbitrary terms.
Frame terms. t[p_{1}->v_{1} ... p_{n}->v_{n}] is a frame term (or simply a frame) if t, p_{1}, ..., p_{n}, v_{1}, ..., v_{n}, n ≥ 0, are arbitrary terms.
Membership, subclass, and frame terms are used to describe objects in object-based logics like F-logic [KLW95]. These terms can be readily mixed both with positional terms and terms with named arguments: p(?X q#r[v(1,2)->s] t(d->e f->g)).
The set of all symbols, Const, is partitioned into positional predicate symbols, predicate symbols with named arguments, positional function symbols, function symbols with named arguments, and individuals. Each positional predicate and function symbol has precisely one arity, which is a non-negative integer that tells how many arguments the symbol can take. An arity for terms with named arguments (of a symbol with named arguments) is a bag {s_{1} ... s_{k}} of argument names (s_{i} ∈ ArgNames). Each predicate or function symbol with named arguments has precisely one arity (for terms with named arguments).
The arity of a symbol (or whether it is a predicate, a function, or an individual) is not specified explicitly in RIF-BLD. Instead, it is inferred as follows. Each constant symbol in a RIF-BLD formula (or a set of formulas) is expected to occur in at most one context: as an individual, a function symbol of a particular arity, a predicate symbol of a particular arity, or an individual. The arity of the symbol and its type is then determined by its context. If a symbol from Const occurs in more than one context, the formula (or a set of formulas) is not considered to be well-formed in RIF-BLD.
Any term (positional or with named arguments) of the form p(...), where p is a predicate symbol, is also an atomic formula. Equality, membership, subclass, and frame terms are also atomic formula. Simple terms (constants and variables) are not formulas. Not all atomic formulas are well-formed -- see Section Well-formedness. A well-formed atomic formula is an atomic formula that is also a well-formed term.
More general formulas are constructed out of the atomic formulas with the help of logical connectives. A formula is a statement that can have one of the following forms:
Atomic: If φ is a well-formed atomic formula then it is also a formula.
Conjunction: If φ_{1}, ..., φ_{n}, n ≥ 0, are formulas then so is And(φ_{1} ... φ_{n}). As a special case, And() is allowed and is treated as a tautology, i.e., a formula that is always true.
Disjunction: If φ_{1}, ..., φ_{n}, n ≥ 0, are formulas then so is Or(φ_{1} ... φ_{n}). When n=0, we get Or() as a special case; it is treated as a formula that is always false.
Existentials: If φ is a formula and ?V_{1}, ..., ?V_{n} are variables then Exists ?V_{1} ... ?V_{n}(φ) is a formula.
Formulas constructed using the above definitions are called RIF-BLD conditions. RIF-BLD rules are defined as follows:
Rule: If φ is an atomic formula and ψ is a RIF-BLD condition then φ :- ψ is a formula, provided that φ does not have the signature bi_atomic (i.e., is not a builtin predicate).
Universals: If φ is a rule and ?V_{1}, ..., ?V_{n} are variables then Forall ?V_{1} ... ?V_{n}(φ) is a formula, called an explicitly quantified rule.
So far, the syntax of RIF-BLD was specified in Mathematical English. Tool developers, however, prefer the more formal EBNF notation, which we will give next. Several points should be kept in mind regarding this notation.
The syntax of first-order logic is not context-free, so EBNF cannot capture the syntax of RIF-BLD precisely. For instance, it cannot capture the well-formedness conditions, i.e., the requirement that each symbol in RIF-BLD can occur in at most one context. As a result, the grammar, below, defines only a superset of RIF-BLD.
The EBNF syntax is not a concrete syntax: it does not address the details of how constants and variables are represented, and it is not sufficiently precise about the delimiters and escape symbols. Instead, white space is informally used as a delimiter, and white space is implied in productions that use Kleene star. For instance, TERM* is to be understood as TERM TERM ... TERM, where each ' ' abstracts from one or more blanks, tabs, newlines, etc. This is done on purpose, since RIF's presentation syntax is intended as a tool for specifying the semantics and for illustration of the main RIF concepts through examples. It is not intended as a concrete syntax for a rule language. RIF defines a concrete syntax only for exchanging rules, and that syntax is XML-based, obtained as a refinement and serialization of the EBNF syntax.
The Condition Language represents formulas that can be used in the body of the RIF-BLD rules. It is supposed to be a common part of a number of RIF dialects, including RIF PRD. The EBNF grammar for a superset of the RIF-BLD condition language is as follows.
CONDITION ::= 'And' '(' CONDITION* ')' | 'Or' '(' CONDITION* ')' | 'Exists' Var+ '(' CONDITION ')' | COMPOUND COMPOUND ::= Uniterm | Equal | Member | Subclass | Frame Uniterm ::= Const '(' (TERM* | (Const '->' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '->' TERM)* ']' TERM ::= Const | Var | COMPOUND Const ::= LITERAL '^^' SYMSPACE Var ::= '?' VARNAME
The production rule for the non-terminal CONDITION represents RIF condition formulas (defined earlier). The connectives And and Or define conjunctions and disjunctions of conditions, respectively. Exists introduces existentially quantified variables. Here Var+ stands for the list of variables that are free in CONDITION. RIF-BLD conditions permit only existential variables, but RIF-FLD syntax allows arbitrary quantification, which can be used in some dialects. A CONDITION can also be a COMPOUND term, i.e. a Uniterm, Equal, Member, Subclass, or Frame. The production for the non-terminal TERM defines RIF-BLD terms -- constants, variables, or COMPOUND terms.
The RIF-BLD presentation syntax does not commit to any particular vocabulary for the names of variables or for the literals used in constant symbols. In the examples, variables are denoted by Unicode character sequences beginning with a ?-sign. Constant symbols have the form: LITERAL^^SYMSPACE, where SYMSPACE is an IRI string that identifies the symbol space of the constant and LITERAL is a Unicode string from the lexical space of that symbol space. Equality, membership, and subclass terms are self-explanatory. Uniterms (Universal terms) are terms that can be either positional or with named arguments. A frame term is a term composed of an object Id and a collection of attribute-value pairs.
Example 1 shows conditions that are composed of uniterms, frames, and existentials. The examples of the frames show that variables can occur in the syntactic positions of object Ids, object properties, or property values.
Example 1 (RIF-BLD conditions) We use the prefix bks to abbreviate http://example.com/books# and the prefix auth for http://example.com/authors#. Positional terms: book^^rif:local(auth:rifwg^^rif:iri bks:LeRif^^rif:iri) Exists ?X (book^^rif:local(?X LeRif^^rif:local)) Terms with named arguments: book^^rif:local(author^^rif:local->auth:rifwg^^rif:iri title^^rif:local->bks:LeRif^^rif:iri) Exists ?X (book^^rif:local(author^^rif:local->?X title^^rif:local->bks:LeRif^^rif:iri)) Frames: wd1^^rif:local[author^^rif:local->auth:rifwg^^rif:iri title^^rif:local->bks:LeRif^^rif:iri ] Exists ?X (wd2^^rif:local[author^^rif:local->?X title^^rif:local->bks:LeRif^^rif:iri ]) Exists ?X (wd2^^rif:local#book^^rif:local[author^^rif:local->?X title^^rif:local->bks:LeRif^^rif:iri]) Exists ?I ?X (?I[author^^rif:local->?X title^^rif:local->bks:LeRif^^rif:iri]) Exists ?I ?X (?I#book^^rif:local[author^^rif:local->?X title^^rif:local->bks:LeRif^^rif:iri]) Exists ?S (wd2^^rif:local[author^^rif:local->auth:rifwg^^rif:iri ?S->bks:LeRif^^rif:iri]) Exists ?X ?S (wd2^^rif:local[author^^rif:local->?X ?S->bks:LeRif^^rif:iri]) Exists ?I ?X ?S (?I#book^^rif:local[author->?X ?S->bks:LeRif^^rif:iri])
The presentation syntax for Horn rules extends the syntax in Section EBNF for RIF-BLD Condition Language with the following productions.
Ruleset ::= RULE* RULE ::= 'Forall' Var+ '(' RULE ')' | Implies | COMPOUND Implies ::= COMPOUND ':-' CONDITION
A Ruleset is a set of RIF rules. Rules are generated by the Implies production, with optional Forall-quantification. Var, COMPOUND, and CONDITION were defined as part of the syntax for positive conditions in Section EBNF for RIF-BLD Condition Language. Note that COMPOUND terms are treated as rules with an empty condition part -- they are usually called facts. Note that, by a definition in Section Formulas, atomic formulas that correspond to builtin predicates (i.e., formulas with signature bi_atomic) are not allowed in the conclusion part of a rule. This restriction is not reflected in the EBNF syntax.
The document RIF Use Cases and Requirements includes a use case "Negotiating eBusiness Contracts Across Rule Platforms", which discusses a business rule slightly modified here:
If an item is perishable and it is delivered to John more than 10 days after the scheduled delivery date then the item will be rejected by him.
In the Presentation EBNF Syntax used throughout this document, this rule can be written in one of these two equivalent ways:
Example 2 (RIF-BLD rules) Here we use the prefix ppl as an abbreviation for http://example.com/people#. The prefix op is used for a yet-to-be-determined IRI, which will be used for RIF builtin predicates. a. Universal form: Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays ( reject^^rif:local(ppl:John^^rif:iri ?item) :- And(perishable^^rif:local(?item) delivered^^rif:local(?item ?deliverydate ppl:John^^rif:iri) scheduled^^rif:local(?item ?scheduledate) fn:subtract-dateTimes-yielding-dayTimeDuration(?deliverydate ?scheduledate ?diffduration) fn:get-days-from-dayTimeDuration(?diffduration ?diffdays) op:numeric-greater-than(?diffdays 10)) ) b. Universal-existential form: Forall ?item ( reject^^rif:local(ppl#John^^rif:iri ?item ) :- Exists ?deliverydate ?scheduledate ?diffduration ?diffdays ( And(perishable^^rif:local(?item) delivered^^rif:local(?item ?deliverydate ppl:John^^rif:iri) scheduled^^rif:local(?item ?scheduledate) fn:subtract-dateTimes-yielding-dayTimeDuration(?deliverydate ?scheduledate ?diffduration) fn:get-days-from-dayTimeDuration(?diffduration ?diffdays) op:numeric-greater-than(?diffdays 10)) ) )
The XML serialization for RIF-BLD presentation syntax given in this section is alternating or fully striped (e.g., Alternating Normal Form). Positional information is optionally exploited only for the arg role elements. For example, role elements (declare and formula) are explicit within the Exists element. Following the examples of Java and RDF, we use capitalized names for class elements and names that start with lowercase for role elements.
The all-uppercase classes in the presentation syntax, such as CONDITION, become XML entities. They act like macros and are not visible in instance markup. The other classes as well as non-terminals and symbols (such as Exists or =) become XML elements with optional attributes, as shown below.
We now serialize the syntax of Section EBNF for RIF-BLD Condition Language in XML.
Classes, roles and their intended meaning - And (conjunction) - Or (disjunction) - Exists (quantified formula for 'Exists', containing declare and formula roles) - declare (declare role, containing a Var) - formula (formula role, containing a CONDITION formula) - Uniterm (term or atomic formula, positional or with named arguments) - Member (member formula) - Subclass (subclass formula) - Frame (Frame formula) - object (Member/Frame role containing a TERM or an object description) - op (Uniterm role for predicates/functions as operations) - arg (argument role) - upper (Member/Subclass upper class role) - lower (Member/Subclass lower instance/class role) - slot (Uniterm/Frame slot role, prefix version of slot infix ' -> ') - Equal (prefix version of term equation '=') - side (Equal left-hand side and right-hand side role) - Const (slot, individual, function, or predicate symbol, with optional 'type' attribute) - Var (logic variable)
For the XML Schema Definition (XSD) of the RIF-BLD condition language see Appendix Specification.
The XML syntax for symbol spaces utilizes the type attribute associated with XML term elements such as Const. For instance, a literal in the xsd:dateTime data type can be represented as <Const type="xsd:dateTime">2007-11-23T03:55:44-02:30</Const>.
The following example illustrates XML serialization of RIF conditions.
Example 3 (A RIF condition and its XML serialization): We use the prefix bks as an abbreviation for http://example.com/books# and curr for http://example.com/currencies# a. RIF condition And ( Exists ?Buyer ( purchase^^rif:local ( ?Buyer ?Seller book^^rif:local ( ?Author bks:LeRif^^rif:iri ) curr:USD^^rif:iri ( 49^^xsd:integer ) ) ?Seller=?Author ) b. XML serialization <And> <formula> <Exists> <declare><Var>Buyer</Var></declare> <formula> <Uniterm> <op><Const type="rif:local">purchase</Const></op> <arg><Var>Buyer</Var></arg> <arg><Var>Seller</Var></arg> <arg> <Uniterm> <op><Const type="rif:local">book</Const></op> <arg><Var>Author</Var></arg> <arg><Const type="rif:iri">bks:LeRif</Const></arg> </Uniterm> </arg> <arg> <Uniterm> <op><Const type="rif:iri">curr:USD</Const></op> <arg><Const type="xsd:integer">49</Const></arg> </Uniterm> </arg> </Uniterm> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And>
The following example illustrates XML serialization of RIF conditions that involve terms with named arguments.
Example 4 (A RIF condition and its XML serialization): We use the prefix bks to abbreviate http://example.com/books#, the prefix auth for http://example.com/authors#, and curr for http://example.com/currencies#, a. RIF condition: And ( Exists ?Buyer ?P ( ?P # purchase^^rif:local [ buyer^^rif:local -> ?Buyer seller^^rif:local -> ?Seller item^^rif:local -> book^^rif:local ( author^^rif:local -> ?Author title^^rif:local -> bks:LeRif^^rif:iri ) price^^rif:local -> 49^^xsd:integer currency^^rif:local -> curr:USD^^rif:iri ] ) ?Seller=?Author ) b. 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:local">purchase</Const></upper> </Member> </object> <slot><Const type="rif:local">buyer</Const><Var>Buyer</Var></slot> <slot><Const type="rif:local">seller</Const><Var>Seller</Var></slot> <slot> <Const type="rif:local">item</Const> <Uniterm> <op><Const type="rif:local">book</Const></op> <slot><Const type="rif:local">author</Const><Var>Author</Var></slot> <slot><Const type="rif:local">title</Const><Const type="rif:iri">bks:LeRif</Const></slot> </Uniterm> </slot> <slot><Const type="rif:local">price</Const><Const type="xsd:integer">49</Const></slot> <slot><Const type="rif:local">currency</Const><Const type="rif:iri">curr:USD</Const></slot> </Frame> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And>
The following extends the XML syntax in Section XML for RIF-BLD Condition Language, by serializing the syntax of Section EBNF for RIF-BLD Rule Language in XML. The Forall element contains the role elements declare and formula, which were earlier used within the Exists element in Section XML for RIF-BLD Condition Language. The Implies element contains the role elements if and then to designate these two parts of a rule.
Classes, roles and their intended meaning - Ruleset (rule collection, containing rule roles) - Forall (quantified formula for 'Forall', containing declare and formula roles) - Implies (implication, containing if and then roles) - if (antecedent role, containing CONDITION) - then (consequent role, containing a Uniterm, Equal, or Frame)
For the XML Schema Definition (XSD) of the RIF-BLD Horn rule language see Appendix Specification.
For instance, the rule in Example 5a can be serialized in XML as shown below as the first element of a rule set whose second element is a business rule for Fred.
Example 5 (A RIF rule set in XML syntax) <Ruleset> <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> <Uniterm> <op><Const type="rif:local">perishable</Const></op> <arg><Var>item</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">delivered</Const></op> <arg><Var>item</Var></arg> <arg><Var>deliverydate</Var></arg> <arg><Const type="rif:iri">ppl:John</Const></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">scheduled</Const></op> <arg><Var>item</Var></arg> <arg><Var>scheduledate</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">fn:subtract-dateTimes-yielding-dayTimeDuration</Const></op> <arg><Var>deliverydate</Var></arg> <arg><Var>scheduledate</Var></arg> <arg><Var>diffduration</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">fn:get-days-from-dayTimeDuration</Const></op> <arg><Var>diffduration</Var></arg> <arg><Var>diffdays</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:iri">op:numeric-greater-than</Const></op> <arg><Var>diffdays</Var></arg> <arg><Const type="xsd:long">10</Const></arg> </Uniterm> </formula> </And> </if> <then> <Uniterm> <op><Const type="xsd:long">reject</Const></op> <arg><Const type="rif:iri">ppl:John</Const></arg> <arg><Var>item</Var></arg> </Uniterm> </then> </Implies> </formula> </Forall> </rule> <rule> <Forall> <declare><Var>item</Var></declare> <formula> <Implies> <if> <Uniterm> <op><Const type="rif:local">unsolicited</Const></op> <arg><Var>item</Var></arg> </Uniterm> </if> <then> <Uniterm> <op><Const type="rif:local">reject</Const></op> <arg><Const type="rif:iri">ppl:Fred</Const></arg> <arg><Var>item</Var></arg> </Uniterm> </then> </Implies> </formula> </Forall> </rule> </Ruleset>
We now show how to translate between the presentation and XML syntaxes of RIF-BLD.
The translation between the presentation syntax and the XML syntax of the RIF-BLD Condition Language is given by a table as follows.
Presentation Syntax | XML Syntax |
---|---|
And ( conjunct_{1} . . . conjunct_{n} ) | <And> <formula>conjunct_{1}</formula> . . . <formula>conjunct_{n}</formula> </And> |
Or ( disjunct_{1} . . . disjunct_{n} ) | <Or> <formula>disjunct_{1}</formula> . . . <formula>disjunct_{n}</formula> </Or> |
Exists variable_{1} . . . variable_{n} ( body ) | <Exists> <declare>variable_{1}</declare> . . . <declare>variable_{n}</declare> <formula>body</formula> </Exists> |
predfunc ( argument_{1} . . . argument_{n} ) | <Uniterm> <op>predfunc</op> <arg>argument_{1}</arg> . . . <arg> argument_{n}</arg> </Uniterm> |
predfunc ( key_{1} -> filler_{1} . . . key_{n} -> filler_{n} ) | <Uniterm> <op>predfunc</op> <slot>key_{1} filler_{1}</slot> . . . <slot>key_{n} filler_{n}</slot> </Uniterm> |
inst [ key_{1} -> filler_{1} . . . key_{n} -> filler_{n} ] | <Frame> <object>inst</object> <slot>key_{1} filler_{1}</slot> . . . <slot>key_{n} filler_{n}</slot> </Frame> |
inst # class [ key_{1} -> filler_{1} . . . key_{n} -> filler_{n} ] | <Frame> <object> <Member> <lower>inst</lower> <upper>class</upper> </Member> </object> <slot>key_{1} filler_{1}</slot> . . . <slot>key_{n} filler_{n}</slot> </Frame> |
sub ## super [ key_{1} -> filler_{1} . . . key_{n} -> filler_{n} ] | <Frame> <object> <Subclass> <lower>sub</lower> <upper>super</upper> </Subclass> </object> <slot>key_{1} filler_{1}</slot> . . . <slot>key_{n} filler_{n}</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> |
name^^space | <Const type="space">name</Const> |
?name | <Var>name</Var> |
The translation between the presentation syntax and the XML syntax of the RIF-BLD Rule Language is given by a table that extends the translation table of Section Translation of RIF-BLD Condition Language as follows.
Presentation Syntax | XML Syntax |
---|---|
Ruleset ( clause_{1} . . . clause_{n} ) | <Ruleset> <rule>clause_{1}</rule> . . . <rule>clause_{n}</rule> </Ruleset> |
Forall variable_{1} . . . variable_{n} ( rule ) | <Forall> <declare>variable_{1}</declare> . . . <declare>variable_{n}</declare> <formula>rule</formula> </Forall> |
conclusion :- condition | <Implies> <if>condition</if> <then>conclusion</then> </Implies> |
*** This is a proposal to specify RIF-CORE etc. by just removing syntactic constructs from RIF-BLD (hence, through The effect of the syntax, restricting the semantics). The point is that it makes more sense for most engines to support only some subdialects of BLD, and that subdialects and fragments of BLD are reused in the definition 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:
RIF-CORE+equality.
RIF-CORE+named arguments.
*** If frames are not included in RIF-CORE / RIF-CORECOND then extensions of RIF-CORE / RIF-CORECOND with frames are added here. |
This section defines the precise relationship between the semantics of RIF-BLD and the semantic framework of RIF-FLD. The remaining sections describe the semantics of RIF-BLD without referring to the general framework -- except for Primitive Data Types whose definition is not duplicated here.
The semantics of the RIF Basic Logic Dialect is defined by specialization from the semantics of the [:FLD/Semantics:Semantic Framework for Logic Dialects] of RIF. Section [:FLD/Semantics#sec-rif-dialect-semantics:Semantics of a RIF Dialect as a Specialization of RIF-FLD] 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.
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.
These two definitions are equivalent for entailment of RIF-BLD conditions by RIF-BLD rulesets, since all rules in RIF-BLD are Horn -- it is a classical result of Van Emden and Kowalski [vEK76].
The set TV of truth values in RIF-BLD consists of just two values, t and f. This set has a total order, called truth order, such that f <_{t} t.
A semantic structure, I, is a tuple of the form <TV, DTS, D, I_{C}, I_{V}, I_{F}, I_{frame}, I_{SF}, I_{sub}, I_{isa}, I_{=}, I_{Truth}>. Here D is a non-empty set of elements called the domain of I, and there is a proper subset, D_{ind} ⊂D, which is used to interpret individuals. We use Const to refer to the set of all constant symbols and Var to refer to the set of all variable symbols. TV denotes the set of truth values that the semantic structure uses and DTS is the set of primitive data types used in I (please refer to Section Primitive Data Types of RIF-FLD for the semantics of data types).
The other components of I are total mappings defined as follows:
I_{C} maps Const to elements of D.
If a constant, c ∈ Const, occurs in the position of an individual then it is required that I_{C}(c) ∈ D_{ind}.
I_{V} maps Var to elements of D_{ind}.
I_{F} maps D to functions D* → D (here D* is a set of all sequences of any finite length over the domain D)
I_{SF} interprets terms with named arguments. It is a total mapping from Const to the set of total functions of the form SetOfFiniteBags(ArgNames × D) → D. This is analogous to the interpretation of positional terms with two differences:
Each pair <s,v> ∈ ArgNames × D represents a argument/value pair instead of just a value in the case of a positional term.
Bags (multisets) are used here because the order of the argument/value pairs in a term with named arguments is immaterial and the pairs may repeat. For instance, p(a->b a->b).
I_{frame} is a total mapping from D to total functions of the form SetOfFiniteBags(D × D) → D.
This mapping interprets frame terms. An argument, d ∈ D, to I_{frame} represent an object and the finite bag {<a1,v1>, ..., <ak,vk>} represents a bag of attribute-value pairs for d. We will see shortly how I_{frame} is used to determine the truth valuation of frame terms.
Bags are used here because the order of the attribute/value pairs in a frame is immaterial and pairs may repeat. For instance, o[a->b a->b].
I_{sub} gives meaning to the subclass relationship. It is a total function D × D → 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.
I_{isa} gives meaning to class membership. It is a total function D × D → 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 cl ## scl must imply o # scl. This is ensured by a restriction in Section Interpretation of Formulas.
I_{=} gives meaning to the equality. It is a total function D × D → D.
I_{Truth} is a total mapping D → TV.
We also define the following mapping I :
I(k) = I_{C}(k), if k is a symbol in Const
I(?v) = I_{V}(?v), if ?v is a variable in Var
I(f(t_{1} ... t_{n})) = I_{F}(I(f))(I(t_{1}),...,I(t_{n}))
I(f(s_{1}->v_{1} ... s_{n}->v_{n})) = I_{SF}(I(f))({<s_{1},I(v_{1})>,...,<s_{n},I(v_{n})>})
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})>})
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))
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_{dt}: 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; and
For each constant lit^^dt ∈ LS_{dt}, I_{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 I_{C} for constants in the lexical spaces that do not correspond to primitive datatypes in DTS.
Truth valuation for well-formed formulas in RIF-BLD is determined using the following function, denoted TVal_{I}:
Positional atomic formulas: TVal_{I}(r(t_{1} ... t_{n})) = I_{Truth}(I(r(t_{1} ... t_{n})))
Atomic formulas with named arguments: TVal_{I}(p(s_{1}->v_{1} ... s_{k}->v_{k})) = I_{Truth}(I(p(s_{1}-> v_{1} ... s_{k}->v_{k}))).
Equality: TVal_{I}(x = y) = I_{Truth}(I(x = y)).
To ensure that equality has precisely the expected properties, it is required that I_{Truth}(I(x = y)) = t if and only if I(x) = I(y) and that I_{Truth}(I(x = y)) = f otherwise.
Subclass: TVal_{I}(sc ## cl) = I_{Truth}(I(sc ## cl)).
To ensure that the operator ## is transitive, i.e., c1 ## c2 and c2 ## c3 imply c1 ## c3, the following is required: For all c1, c2, c3 ∈ D, min_{t}(TVal_{I}(c1 ## c2), TVal_{I}(c2 ## c3)) ≤_{t} TVal_{I}(c1 ## c3).
Membership: TVal_{I}(o # cl) = I_{Truth}(I(o # cl)).
To ensure that all members of a subclass are also members of the superclass, i.e., o # cl and cl ## scl implies o # scl, the following is required: For all o, cl, scl ∈ D, min_{t}(TVal_{I}(o # cl), TVal_{I}(cl ## scl)) ≤_{t} TVal_{I}(o # scl).
Frame: TVal_{I}(o[a_{1}->v_{1} ... a_{k}->v_{k}]) = I_{Truth}(I(o[a_{1}->v_{1} ... a_{k}->v_{k}])).
TVal_{I}(o[a_{1}->v_{1} ... a_{k}->v_{k}]) = min_{t}(TVal_{I}(o[a_{1}->v_{1}]), ..., TVal_{I}(o[a_{k}->v_{k}]))
Conjunction: TVal_{I}(And(c_{1} ... c_{n})) = min_{t}(TVal_{I}(c_{1}), ..., TVal_{I}(c_{n})).
Disjunction: TVal_{I}(Or(c_{1} ... c_{n})) = max_{t}(TVal_{I}(c_{1}), ..., TVal_{I}(c_{n})).
Quantification: TVal_{I}(Exists ?v_{1} ... ?v_{n} (φ)) = max_{t}(TVal_{I*}(φ)) and TVal_{I}(Forall ?v_{1} ... ?v_{n} (φ)) = min_{t}(TVal_{I*}(φ)).
Here max_{t} (respectively, min_{t}) is taken over all interpretations I* of the form <TV, DTS, D, I_{C}, I*_{V}, I_{F}, I_{frame}, I_{SF}, I_{sub}, I_{isa}, I_{Truth}>, which are exactly like I, except that the mapping I*_{V}, is used instead of I_{V}. I*_{V} is defined to coincide with I_{V} on all variables except, possibly, on ?v_{1},...,?v_{n}.
Rules: TVal_{I}(conclusion :- condition) = t, if TVal_{I}(conclusion) ≥_{t} TVal_{I}(condition); TVal_{I}(conclusion :- condition) = f otherwise.
A model of a set Ψ of formulas is a semantic structure I such that TVal_{I}(φ) = t for every φ∈Ψ. In this case, we write I |= Ψ.
We now define what it means for a set of RIF-BLD rules to entail a RIF-BLD condition.
Let R be a set of RIF-BLD rules and φ an existentially closed RIF-BLD condition formula. We say that R entails φ, written as R |= φ, if and only if for every semantic structure I of R and every ψ ∈ R, it is the case that TVal_{I}(ψ) ≤ TVal_{I}(φ).
Equivalently, we can say that R |= φ holds iff whenever I |= R it follows that also I |= φ.
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, 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 Vocabulary Description Language 1.0: RDF Schema, Brian McBride , Editor, W3C Recommendation 10 February 2004, http://www.w3.org/TR/rdf-schema/.
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 - Internationalized Resource Identifiers (IRIs), M. Duerst and M. Suignard, IETF, January 2005. This document is http://www.ietf.org/rfc/rfc3987.txt.
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/.
Normal Form Conventions for XML Representations of Structured Data, Henry S. Thompson. October 2001.
Logical foundations of object-oriented and frame-based languages, M. Kifer, G. Lausen, J. Wu. Journal of ACM, July 1995, pp. 741--843.
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.
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.
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/.
Nonmonotonic logics: meaning and utility, Y. Shoham. Proc. 10th International Joint Conference on Artificial Intelligence, Morgan Kaufmann, pp. 388--393, 1987.
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.
FLORA-2: An Object-Oriented Knowledge Base Language, M. Kifer. Web site. Available at http://flora.sourceforge.net.
Object-Oriented jDREW, Web site. Available at http://www.jdrew.org/oojdrew/.
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.
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.
The semantics of predicate logic as a programming language, M. van Emden and R. Kowalski. Journal of the ACM 23 (1976), 733-742.
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.7 2008-02-12 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: CONDITION ::= 'And' '(' CONDITION* ')' | 'Or' '(' CONDITION* ')' | 'Exists' Var+ '(' CONDITION ')' | COMPOUND COMPOUND ::= Uniterm | Equal | Member | Subclass | Frame Uniterm ::= Const '(' (TERM* | (Const '->' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '->' TERM)* ']' TERM ::= Const | Var | COMPOUND Const ::= LITERAL '^^' SYMSPACE Var ::= '?' VARNAME </xs:documentation> </xs:annotation> <xs:group name="CONDITION"> <!-- CONDITION ::= 'And' '(' CONDITION* ')' | 'Or' '(' CONDITION* ')' | 'Exists' Var+ '(' CONDITION ')' | COMPOUND --> <xs:choice> <xs:element ref="And"/> <xs:element ref="Or"/> <xs:element ref="Exists"/> <xs:group ref="COMPOUND"/> </xs:choice> </xs:group> <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="CONDITION"/> </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="COMPOUND"> <!-- COMPOUND ::= Uniterm | Equal | Member | Subclass | Frame --> <xs:choice> <xs:element ref="Uniterm"/> <xs:element ref="Equal"/> <xs:element ref="Member"/> <xs:element ref="Subclass"/> <xs:element ref="Frame"/> </xs:choice> </xs:group> <xs:element name="Uniterm"> <!-- Uniterm ::= Const '(' (TERM* | (Const '->' TERM)*) ')' --> <xs:complexType> <xs:sequence> <xs:element ref="op"/> <xs:choice> <xs:element ref="arg" minOccurs="0" maxOccurs="unbounded"/> <xs:element ref="slot" minOccurs="0" maxOccurs="unbounded"/> </xs:choice> </xs:sequence> </xs:complexType> </xs:element> <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:sequence> <xs:element ref="Const"/> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Equal"> <!-- Equal ::= TERM '=' TERM --> <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"> <!-- Member ::= TERM '#' TERM --> <xs:complexType> <xs:sequence> <xs:element ref="lower"/> <xs:element ref="upper"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Subclass"> <!-- Subclass ::= TERM '##' TERM --> <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"> <!-- Frame ::= TERM '[' (TERM '->' TERM)* ']' --> <xs:complexType> <xs:sequence> <xs:element ref="object"/> <xs:element name="slot" minOccurs="0" maxOccurs="unbounded"> <!-- note difference from slot in Uniterm --> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="object"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="TERM"> <!-- TERM ::= Const | Var | COMPOUND --> <xs:choice> <xs:element ref="Const"/> <xs:element ref="Var"/> <xs:group ref="COMPOUND"/> </xs:choice> </xs:group> <xs:element name="Const"> <!-- Const ::= LITERAL '^^' SYMSPACE --> <xs:complexType mixed="true"> <xs:sequence/> <xs:attribute name="type" type="xs:string" use="required"/> </xs:complexType> </xs:element> <xs:element name="Var" type="xs:string"> <!-- Var ::= '?' VARNAME --> </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.7 2008-02-12 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 ::= Ruleset* Ruleset ::= RULE* RULE ::= 'Forall' Var+ '(' RULE ')' | Implies | COMPOUND Implies ::= COMPOUND ':-' CONDITION Note that this is an extension of the syntax for the RIF-BLD Condition Language (BLDCond.xsd). </xs:documentation> </xs:annotation> <!-- The Rule Language includes the Condition Language--> <xs:include schemaLocation="BLDCond.xsd"/> <xs:element name="Document"> <!-- Document ::= Ruleset* --> <xs:complexType> <xs:sequence> <xs:element ref="Ruleset" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Ruleset"> <!-- Ruleset ::= RULE* --> <xs:complexType> <xs:sequence> <xs:element ref="rule" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="rule"> <xs:complexType> <xs:sequence> <xs:group ref="RULE"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="RULE"> <!-- RULE ::= 'Forall' Var+ '(' RULE ')' | Implies | COMPOUND --> <xs:choice> <xs:element ref="Forall"/> <xs:element ref="Implies"/> <xs:group ref="COMPOUND"/> </xs:choice> </xs:group> <xs:element name="Forall"> <xs:complexType> <xs:sequence> <xs:element ref="declare" minOccurs="1" maxOccurs="unbounded"/> <!-- note different from formula in And, Or and Exists --> <xs:element name="formula"> <xs:complexType> <xs:group ref="RULE"/> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Implies"> <!-- Implies ::= COMPOUND ':-' CONDITION --> <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="CONDITION"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="then"> <xs:complexType> <xs:sequence> <xs:group ref="COMPOUND"/> </xs:sequence> </xs:complexType> </xs:element> </xs:schema>