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.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 52 documents:
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 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,frames
a lá F-logic [KLW95],
internationalized resource identifiers (or IRIs, defined by
RFC 3987 [ RFC 3987RFC-3987]) as identifiers for
concepts, and XML Schema data types. In addition, the last twodocument
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
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.
One important 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 uses in other dialects of 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.
RIF-BLD is defined in two different ways.ways -- both
normative. First, it is defined as a specialization of RIF-FLD,the
RIF Framework for
Logic-based Dialects ; it is a(RIF-FLD) -- the RIF extensibility
framework. 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. WithAll
logic-based dialects are required to specialize this framework, one can extend RIF-BLD with default negation, higher-order features, and so on.framework.
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 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. The reader who is not interested in how RIF-BLD is derived from the framework can skip this section and proceed to Direct Specification of RIF-BLD Syntax.
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. Thesyntax of the RIF Basic Logic Dialect is defined by
specialization from the syntax of the RIF
Syntactic Framework for Logic Dialects of RIF.. Section Syntax of a
RIF Dialect as a Specialization of RIF-FLDthe RIF Framework in that
document lists the parameters of the syntactic framework, which we
will now specialize for RIF-BLD.
The signature set of RIF-BLD contains the following signatures:
, bi_atomic{ } , where bi_atomic < atomic .The signature term{ }individual{ } represents the context
in which individual objects (but not atomic formulas) can
appear.
The signature bi_atomic{ }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 havethe signaturecontext where
atomic rather than bi_atomic .formulas can occur.
These represent function symbols of arity n , user-definedand predicate symbols of arity
n , and n -ary builtin predicates, respectively. For every set(each of symbols s1 ,..., sk ∈ SigNames ,the above cases has n
individuals 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, a builtinan externally defined predicate of one particular
arity, or aan 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 termindividual; 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.
Note 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 extraspecial syntax for declaring signatures.
Instead, the author specifies signatures are inferredcontextually. That
is, since RIF-BLD requires that each symbol is associated with a
unique signature, the signature can beis determined from the context in
which the symbol is used. If a symbol is used in more than one
context, the parser shouldmust treat itthis as a syntax error. If no errors
are found, all terms and atomic formulas are guaranteed to be
well-formed. As a consequence,Thus, signatures are not part of the RIF-BLD
languagelanguage, and term , atomic ,individual and bi_atomicatomic are not
reserved keywords in RIF-BLD.
RIF-BLD supports all the symbol spaces defined in Section Symbol Spaces of the syntactic framework:
RIF-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 head or the body.
|
This normative section defines the symbols = , # , ## , -> , :- , and auxiliary symbols, such as "(" and ")".precise relationship between
the setsemantics of connective symbols, quantifiers, = , etc., is disjoint from ConstRIF-BLD and Var . Variables are written as Unicode strings preceded withthe symbol "?".semantic framework of RIF-FLD.
Specification of the syntax for constant symbolssemantics without reference to RIF-FLD is
given in Section Symbol SpacesDirect Specification of RIF-FLD.RIF-BLD Semantics.
The languagesemantics of RIF-BLDthe RIF Basic Logic Dialect is defined by
specialization from the setsemantics of formulas constructed usingthe above alphabet accordingSemantic 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 rules spelled out below. 2.3 Terms RIF-BLD supports several kindssemantics of terms: constants and variables , positional terms, terms with named arguments , equality , membership , and subclass terms, and framesa dialect is derived
from these notions by specializing the following parameters.
RIF-BLD does not support negation. This is the word " term " will be used to referonly obvious
simplification with respect to any kind of terms. Formally, terms are definedRIF-FLD as follows: Constants and variables . If t ∈ Const or t ∈ Var then tfar as the semantics is
a simple term . Positional termsconcerned.
IfThe set TV of truth values in RIF-BLD consists of
just two values, t ∈ Constand f such that f
<t 1 , ...,t n are terms then t(t 1 .... Clearly, <t n )is a positional termtotal
order here.
Terms with named argumentsRIF-BLD supports all the data types listed in Section Primitive Data
Types of RIF-FLD:
A term with named arguments (a term with named arguments)Recall that logical entailment in RIF-FLD is of the form t(s 1 ->v 1 ... s n ->v n ) , where t ∈ Const , v 1 , ..., v n are terms (positional,defined with
named arguments, frame, etc.),respect to an unspecified set of intended semantic structures and
s 1 , ..., s n are (not necessarily distinct) symbols from thethat dialects of RIF must make this notion concrete. For RIF-BLD,
this set ArgNames .is defined in one of the term t here representstwo following equivalent
ways:
These two definitions are named and their orderequivalent for entailment of RIF-BLD
conditions by RIF-BLD sets of formulas, since all rules in RIF-BLD
are Horn -- it is immaterial. Note thata term like f() is both positionalclassical result of Van Emden and with named arguments. Equality terms . If tKowalski
[vEK76].
The list of supported data types will move to another document,
Data Types and
|
This normative section specifies the syntax of RIF-BLD directly,
without referring to RIF-FLD. We define both a membership term if tpresentation
syntax and s are arbitrary terms. Subclass terms . t##san XML syntax. The presentation syntax is not
intended to be a subclass term if t and s are arbitrary terms. Frame terms . t[p 1 ->v 1 ... p n ->v n ]concrete syntax for RIF-BLD. It 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,defined in
Mathematical English and frame terms are usedis intended to describe objects in object-based logics like F-logic [ KLW95 ]. These terms canbe readily mixed both with positional termsused in the definitions
and terms with named arguments: p(?X q#r[v(1,2)->s] t(d->e f->g)) . 2.4 Well-formednessexamples. This syntax deliberately leaves out details such as
the setdelimiters 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 argumentsthe symbol can take. An arity for terms with named arguments (of a symbol with named arguments) is a bag {s 1 ... s k }various syntactic components, escape symbols,
parenthesizing, precedence of argument names ( s i ∈ ArgNames ). Each predicate or function symbol with named arguments has precisely one arity (for terms with named arguments).operators, and the arity of a symbol (or whether itlike. Since RIF is
a predicate, a function, oran individual) is not specified explicitly in RIF-BLD. Instead,interchange format, it is inferreduses XML as follows. Each constant symbol in aits concrete syntax.
formula (orDefinition
(Alphabet). The alphabet of RIF-BLD consists
of
The set of connective symbols, quantifiers, =, etc., is
then determined by its context. If a symboldisjoint from Const occurs in more than one context,and Var. The formula (or a set of formulas) is not considered to be well-formedargument names
in RIF-BLD. 2.5 Formulas Any term (positional orArgNames are written as unicode strings that must not
start with a question mark, "?". Variables are written as
Unicode strings preceded with named arguments) ofthe form p(...)symbol "?".
Constants are written as "literal"^^symspace, where
pliteral is a predicate symbol,sequence of Unicode characters and
symspace is alsoan atomic formulaidentifier for a symbol space. Symbol
spaces are defined in Section Symbol
Spaces of the RIF-FLD document.
The definition of symbol spaces will eventually be also given in the document Data Types and Builtins, so the above reference will be to that document instead of RIF-FLD. |
The symbols =, #, and ## are used in
formulas that define equality, class membership, subclass,and frame terms are also atomic formula. Simplesubclass
relationships. The symbol -> is used in terms (constantsthat have
named arguments and variables) are notin frame formulas. Not all atomic formulas are well-formed -- see Section Well-formedness . A well-formed atomic formula isThe symbol External
indicates that an atomic formula thator a function term is alsodefined
externally (e.g., a well-formed term. More general formulas are constructed out ofbuiltin).
The atomic formulassymbol Group is used to organize RIF-BLD rules into
collections and annotate them with metadata. ☐
The helplanguage of logical connectives. A formulaRIF-BLD is a statement that can have one ofthe following forms: Atomic : If φ is a well-formed atomic formula then it is also a formula. Conjunction : If φ 1 , ..., φ n , n ≥ 0, areset of formulas then so is And( φ 1 ... φ n ) . As a special case, And() is allowedconstructed using
the above alphabet according to the rules given below.
RIF-BLD supports several kinds of terms: constants and
is treated as a tautology, i.e., a formula that is always true. Disjunction : If φ 1variables, ..., φ npositional terms, terms with named
arguments, n ≥ 0, are formulas then so is Or( φ 1 ... φ n ) . When n=0equality, we get Or() as a special case; it is treated as a formula that is always false. Existentials :membership, and
subclass atomic formulas, and frame formulas. The
word "term" will be used to refer to any kind of these
constructs.
Definition (Term).
The syntax of RIF-BLD was specified in Mathematical English. Tool developers, however, preferterm t here represents a predicate or a function;
s1, ..., sn represent
argument names; and v1, ...,
vn represent argument values. The more formal EBNF notation, which we will give next. Several points shouldargument
names, s1, ..., sn, are
required to be kept in mind regarding this notation.pairwise distinct. Terms with named arguments are
like positional terms except that the syntax of first-order logicarguments are named and their
order 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 requirementimmaterial. Note that each symbol in RIF-BLD can occur in at most one context. As a result, the grammar, below, defines onlya supersetterm of RIF-BLD.the EBNF syntaxform f() is
not a concrete syntax: it does not address the details of how constantsboth positional and variables are represented,with named arguments.
Such terms are used for exchanging rules,representing builtin functions and
that syntax is XML-based, obtainedpredicates as a refinementwell as "procedurally attached" terms or predicates,
which might exist in various rule-based systems, but are not
specified by RIF. ☐
Membership, subclass, and serialization of the EBNF syntax. 2.6.1 EBNF for RIF-BLD Condition Language The Condition Language represents formulas that can beframe terms are used in the body of the RIF-BLD rules. It is supposedto be a common part of a numberdescribe
objects and class hierarchies.
The EBNF grammar for a supersetset of the RIF-BLD condition languageall symbols, Const, 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 ::= '?' VARNAMEpartitioned into
The production rule forsymbols in Const that belong to the non-terminal CONDITION representssupported RIF
condition formulas (defined earlier). The connectives And and Or define conjunctionsdata types are individuals.
Each predicate and disjunctions of conditions, respectively. Exists introduces existentially quantified variables. Here Var+ standsfunction symbol has precisely one
arity.
The arity of a symbol (or whether it is a predicate, a function,
or an individual) is not specified in CONDITION .RIF-BLD conditions permit only existential variables, but RIF-FLD syntax allows arbitrary quantification, which can be usedexplicitly. Instead,
it is inferred as follows. Each constant symbol in some dialects.a CONDITION can also beRIF-BLD
formula (or a COMPOUND term, i.e.set of formulas) may occur in at most one context: as
an individual, a Uniterm , Equal , Member , Subclass ,function symbol of a particular arity, or Frame .a
predicate symbol of a particular arity. The production forarity of the non-terminal TERM defines RIF-BLD terms -- constants, variables, or COMPOUND terms.symbol and
its type is then determined by its context. If a symbol from
Const occurs in more than one context in a set of
formulas, the RIF-BLD presentation syntax doesset is not commit to any particular vocabularywell-formed in RIF-BLD.
For the namesa term of variables or forthe literals used in constant symbols.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 Defined Terms of RIF-FLD.
Also, if a term of the examples, variables are denoted by Unicode character sequences beginning with a ?-sign. Constant symbols have the form: LITERAL^^SYMSPACE , where SYMSPACE isform External(p(...)) occurs as
an IRI string that identifiesatomic formula then the symbol spaceoccurrence of the constant and LITERALp is considered
to be a Unicode string frompredicate occurrence.
The |
Any term (positional or with named arguments) of the form
p(...) (or External(p(...)), where p is
a predicate symbol, is also an atomic formula.
Equality, membership, subclass, and subclassframe terms are self-explanatory. Uniterms ( Universalalso atomic
formulas. A formula of the form External(p(...)) is also
called an externally defined atomic formula.
Simple terms )(constants and variables) are terms that can be either positional or with named arguments.not formulas.
Not all atomic formulas are well-formed. A frame termwell-formed atomic
formula is an atomic formula that is also a well-formed
term composed(see Section Well-formedness of an object Id and a collection of attribute-value pairs. Example 1 shows conditions thatTerms). More general formulas are
composedconstructed out of uniterms, frames, and existentials.the examples ofatomic formulas with the frames showhelp of logical
connectives.
Definition
(Well-formed formula). A well-formed formula is a
statement that variables can occur in the syntactic positionshas one 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]) 2.6.2 EBNF for RIF-BLD Rule Language The presentation syntax for Horn rules extends the syntax in Section EBNF for RIF-BLD Condition Language withthe following productions. Ruleset ::= RULE* RULE ::= 'Forall' Var+ '(' RULE ')' | Implies | COMPOUND Implies ::= COMPOUND ':-' CONDITIONforms:
Formulas constructed using the conclusion partabove definitions are called
RIF-BLD
conditions. The following formulas lead to the
notion of a RIF-BLD rule.
Group formulas are intended to represent sets of rules annotated
with metadata. This metadata is specified using an optional frame
term φ. Note that some of the Exists element. Followingρi's can
be group formulas themselves, which means that groups can be
nested. This allows one to attach metadata to various subsets of
rules, which may be inside larger rule sets, which in turn can be
annotated. ☐
It can be seen from the examplesdefinitions that RIF-BLD has a wide
variety of Java and RDF, we use capitalized namessyntactic forms for class elementsterms and namesformulas. This provides
the infrastructure for exchanging rule languages that start with lowercasesupport rich
collections of syntactic forms. Systems that do not support some of
that syntax directly can still support it through syntactic
transformations. For role elements. The all-uppercase classesinstance, disjunctions in the presentation syntax,rule body can be
eliminated through a standard transformation, 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 elementsreplacing
p :- Or(q r) with optional attributes, as shown below. 2.7.1 XML for RIF-BLD Condition Language 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 containinga 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)pair of the RIF-BLD condition language see Appendix Specificationrules p :- q,
p :- r. Terms with named arguments can be reduced
to positional terms by ordering the XML syntax for symbol spaces utilizesarguments by their names and
incorporating them into the type attribute associated with XML term elements such as Const .predicate name. For instance,
a literal in the xsd:dateTime data typep(bb->1 aa->2) can be represented as
<Const type="xsd:dateTime">2007-11-23T03:55:44-02:30</Const>p_aa_bb(2,1).
So far, the syntax of Section EBNF forRIF-BLD Rule Languagehas been specified in XML. The Forall element contains the role elements declare and formula ,Mathematical
English. Tool developers, however, may prefer EBNF notation, which
were earlier used withinprovides a more succinct overview of the Exists elementsyntax. Several points
should be kept in Section XML for RIF-BLD Condition Language . The Implies element containsmind regarding this notation.
The translation betweenCondition Language represents formulas that can be used in
the presentation syntax andbody of the XML syntaxRIF-BLD rules. It is intended 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 given by a tableas follows.
PresentationSyntaxXMLSyntaxAnd(conjunct1...conjunctn)<And><formula>conjunctFORMULA ::= 'And' '(' FORMULA* ')' | 'Or' '(' FORMULA* ')' | 'Exists' Var+ '(' FORMULA ')' | ATOMIC | 'External' '(' Atom ')' ATOMIC ::= Atom | Equal | Member | Subclass | Frame Atom ::= UNITERM UNITERM ::= Const '(' (TERM* | (Name '->' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '->' TERM)* ']' TERM ::= Const | Var | Expr | 'External' '(' Expr ')' Expr ::= UNITERM Const ::= '"' UNICODESTRING '"^^' SYMSPACE Name ::= UNICODESTRING Var ::= '?' UNICODESTRING
The production rule for the non-terminal FORMULA 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 FORMULA. RIF-BLD conditions permit only existential variables, but RIF-FLD Syntax allows arbitrary quantification, which can be used in some dialects. A RIF-BLD FORMULA can also be an ATOMIC term, i.e. an Atom, External Atom, Equal, Member, Subclass, or Frame. A TERM can be a constant, variable, Expr, or External Expr.
The RIF-BLD presentation syntax does not commit to any particular vocabulary except for using Unicode strings in constant symbols, as names, and for variables. Constant symbols have the form: "UNICODESTRING"^^SYMSPACE, where SYMSPACE is an IRI string that identifies the symbol space of the constant and UNICODESTRING is a Unicode string from the lexical space of that symbol space. Names are just denoted by Unicode character sequences. Variables are denoted by Unicode character sequences beginning with a ?-sign. Equality, membership, and subclass terms are self-explanatory. An Atom and Expr (expression) can either be positional or with named arguments. A frame term is a term composed of an object Id and a collection of attribute-value pairs. An External Atom is a call to an externally defined predicate of RIF-DTB. Likewise, an External Expr is a call to an externally defined function of RIF-DTB.
Example 1 </formula>(RIF-BLD conditions).
This example shows conditions that are composed of atoms, expressions, frames, and existentials. In frame formulas variables are shown in the positions of object Ids, object properties, or property values. For brevity, we use the compact URI notation [CURIE], prefix:suffix, which should be understood as a macro that expands into a concatenation of the prefix definition and suffix. Thus, if bks is a 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 compact URI notation is not part of the RIF-BLD syntax.
Compact URI prefixes: bks expands into http://example.com/books# auth expands into http://example.com/authors# cpt expands into http://example.com/concepts#
Positional terms: "cpt:book"^^rif:iri("auth:rifwg"^^rif:iri "bks:LeRif"^^rif:iri) Exists ?X ("cpt:book"^^rif:iri(?X "bks:LeRif"^^rif:iri)) Terms with named arguments: "cpt:book"^^rif:iri(cpt:author->"auth:rifwg"^^rif:iri cpt:title->"bks:LeRif"^^rif:iri) Exists ?X ("cpt:book"^^rif:iri(cpt:author->?X cpt:title->"bks:LeRif"^^rif:iri)) Frames: "bks:wd1"^^rif:iri["cpt:author"^^rif:iri->"auth:rifwg"^^rif:iri "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri] Exists ?X ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]) Exists ?X ("bks:wd2"^^rif:iri # "cpt:book"^^rif:iri["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]) Exists ?I ?X (?I["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]) Exists ?I ?X (?I # "cpt:book"^^rif:iri["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]) Exists ?S ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->"auth:rifwg"^^rif:iri ?S->"bks:LeRif"^^rif:iri]) Exists ?X ?S ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->?X ?S->"bks:LeRif"^^rif:iri]) Exists ?I ?X ?S (?I # "cpt:book"^^rif:iri[author->?X ?S->"bks:LeRif"^^rif:iri])
The presentation syntax for Horn rules extends the syntax in Section EBNF for RIF-BLD Condition Language with the following productions.
Group ::= 'Group' IRIMETA? '(' (RULE | Group)* ')' IRIMETA ::= Frame RULE ::= 'Forall' Var+ '(' CLAUSE ')' | CLAUSE CLAUSE ::= Implies | ATOMIC Implies ::= ATOMIC ':-' FORMULA
For convenient reference, we reproduce the condition language part of the EBNF below.
FORMULA ::= 'And' '(' FORMULA* ')' | 'Or' '(' FORMULA* ')' | 'Exists' Var+ '(' FORMULA ')' | ATOMIC | 'External' '(' Atom ')' ATOMIC ::= Atom | Equal | Member | Subclass | Frame Atom ::= UNITERM UNITERM ::= Const '(' (TERM* | (Name '->' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '->' TERM)* ']' TERM ::= Const | Var | Expr | 'External' '(' Expr ')' Expr ::= UNITERM Const ::= '"' UNICODESTRING '"^^' SYMSPACE Name ::= UNICODESTRING Var ::= '?' UNICODESTRING
A RIF-BLD Group is a nested collection of RIF-BLD rules
annotated with optional metadata, IRIMETA, represented as
Frames. A Group can contain any number of
RULEs along with any number of nested Groups.
Rules are generated by CLAUSE, which can be in the scope
of a Forall quantifier. If a CLAUSE in the
RULE production has a free (non-quantified) variable, it
must occur in the Var+ sequence. Frame,
Var, ATOMIC, and FORMULA were defined as
part of the syntax for positive conditions in Section EBNF for RIF-BLD Condition
Language. In the CLAUSE production an ATOMIC
is treated as a rule with an empty condition part -- in which case
it is usually called a fact. Note that, by a definition in
Section Formulas, formulas
that query externally defined atoms (i.e., formulas of the form
External(Atom(...))) are not allowed in the conclusion
part of a rule (ATOMIC does not expand to
External).
Example 2 (RIF-BLD rules).
This example shows a business rule borrowed from the document RIF Use Cases and Requirements:
As before, 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))) ) b. Universal-existential form: Forall ?item ( "cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item ) :- 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 annotated with metadata).
This example shows a group formula that consists of two RIF-BLD rules. The first of these rules is copied from Example 2a. The group 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 normative section specifies the semantics of RIF-BLD directly, without referring to RIF-FLD.
The set TV of truth values in RIF-BLD consists of just two values, t and f.
The key concept in a model-theoretic semantics of a logic language is the notion of a semantic structure. The definition, below, is a little bit more general than necessary. This is done in order to better see the connection with the semantics of the RIF framework.
Definition (Semantic structure). A semantic structure, I, is a tuple of the form <TV, DTS, D, Dind, Dfunc, IC, IV, IF, Iframe, ISF, Isub, Iisa, I=, Iexternal, Itruth>. Here D is a non-empty set of elements called the domain of I, and Dind, Dfunc are nonempty subsets of D. Dind is used to interpret the elements of Const, which denote individuals and Dfunc is used to interpret the elements of Const that denote function symbols. As before, Const denotes the set of all constant symbols and Var 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:
This mapping interprets constant symbols. In addition:
This mapping interprets variable symbols.
This mapping interprets positional terms. In addition:
This mapping interprets function symbols with named arguments. In addition:
This mapping interprets frame terms. An argument, d ∈ Dind, to Iframe 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 Iframe is used to determine the truth valuation of frame terms.
Bags (multi-sets) are used here because the order of the attribute/value pairs in a frame is immaterial and pairs may repeat: o[a->b a->b]. Such repetitions arise naturally when variables are instantiated with constants. For instance, o[?A->?B ?A->?B] becomes o[a->b a->b] if variable ?A is instantiated with the symbol a and ?B with b.
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.
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.
It gives meaning to the equality operator.
<formula> conjunctIt is used to define truth valuation for formulas.
For every external schema, σ, associated with the language, Iexternal(σ) is assumed to be specified externally in some document (hence the name external schema). In particular, if σ is a schema of a RIF builtin predicate or function, Iexternal(σ) is specified in the document Data Types and Builtins so that:
For convenience, we also define the following mapping I from terms to D:
Here we use {...} to denote a set of argument/value pairs.
Here {...} denotes 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 structurebag of RIF-BLD suggests several useful subdialects: RIF-CORE . This subdialectattribute/value pairs.
This subdialect extends RIF-CORENote that, by adding syntactic support for terms with named arguments.definition, External(t) is well formed
only if frames are not included in RIF-CORE / RIF-CORECOND then extensions of RIF-CORE / RIF-CORECOND with frames are added here. 3 RIF-BLD Semantics 3.1 The Semantics of RIF-BLD as a Specialization of RIF-FLD 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 definitiont is not duplicated here. The semanticsan instance of the RIF Basic Logic Dialect is definedan external schema.
Furthermore, by specialization from the semantics ofthe [:FLD/Semantics:Semantic Framework for Logic Dialects] of RIF. Section [:FLD/Semantics#sec-rif-dialect-semantics:Semantics of a RIF Dialect as a Specializationdefinition of RIF-FLD] in that document lists the parameterscoherent sets of the semantic framework, which we need to specialize for RIF-BLD. Recall that the semanticsexternal schemas,
t can be an instance of a dialectat most one such schema, so
I(External(t)) is derived from these notions by specializing the following parameters.well-defined.
The effect of data types. The syntax . RIF-BLD does not support negation. This is the only obvious simplification with respect to RIF-FLD as far asdata types in
DTS impose the semanticsfollowing restrictions. If dt
is concerned. Truth values . The set TV of truth values in RIF-BLD consistsa symbol space identifier of just two values, t and f such that f < t t . Clearly, < t isa total order here.data types . RIF-BLD supports alltype, let
LSdt denote the data types listed inlexical space of
dt, VSdt denote its value space,
and Ldt: LSdt →
VSdt the lexical-to-value-space mapping
(for the definitions of these concepts, see Section Primitive Data
Types of RIF-FLD: xsd:long xsd:integer xsd:decimal xsd:string xsd:time xsd:dateTime rdf:XMLLiteral rif:text Logical entailment . Recall that logical entailment in RIF-FLD is defined with respect to an unspecified set of intended semantic structuresRIF-FLD). Then the following must hold:
That dialects of RIFis, IC must make this notion concrete.map the constants of a
data type dt in accordance with
Ldt.
RIF-BLD does not impose restrictions on
IC for RIF-BLD, this set is definedconstants in one ofthe two following equivalent ways: as a setlexical spaces
that do not correspond to primitive datatypes in DTS.
☐
Definition
(Truth valuation). Truth valuation for
entailment of RIF-BLD conditions by RIF-BLD rulesets, since all ruleswell-formed formulas in RIF-BLD are Horn -- itis a classical result of Van Emden and Kowalski [ vEK76 ]. 3.2determined using the following
function, denoted TValI:
To ensure that the operator ## is a tuple oftransitive, i.e.,
c1 ## c2 and c2 ## c3 imply
c1 ## c3, the form < TVfollowing is required:
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:
Since the set of all constant symbols and Var to referdifferent attribute/value pairs are supposed to be
understood as conjunctions, the set of all variable symbols. TV denotes the set of truth values that the semantic structure uses and DTSfollowing is the set of primitive data types used inrequired:
This mapping interprets constant symbols.Note that, by definition, External(t) is well-formed
only if a constant, c ∈ Const , occurs int is an instance of an external schema.
Furthermore, by the positiondefinition of coherent sets of external schemas,
t can be an individual then itinstance of at most one such schema, so
I(External(t)) is required thatwell-defined.
The empty conjunction is treated as a set of all sequences of any finite length over the domain Dtautology, so
TValI(And()) This mapping interprets positional terms.= t.
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. The arguments of a term with named arguments constitute a finite bag of argument/value pairs rather than a finite ordered sequence of simple elements. Bags (multisets) are used here because the order ofThe argument/value pairs in a term with named argumentsempty disjunction is immaterialtreated as a contradiction, so
TValI(Or()) = f.
Here I* is a total mapping from D to total functionssemantic structure of the form
SetOfFiniteBags ( D × D ) →<TV, DTS, D . This mapping interprets frame terms. An argument,,
D ∈ind, Dfunc,
toI 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 howC, I*V,
IF, Iframe,
ISF, Isub,
Iisa, I=,
Iexternsl,
Itruth>, which is used to determineexactly like
I, except that the truth valuation of frame terms. Bags aremapping
I*V, is used here because the orderinstead of
the attribute/value pairs in a frameIV. I*V is
immaterial and pairs may repeat. For instance, o[a->b a->b]defined to coincide with IV on all
variables except, possibly, on
?v1,...,?vn.
If Γ is a total function D × D → D .group formula of the operator ## is required to be transitive, i.e., c1 ## c2form Group φ
(ρ1 ... ρn) or Group (ρ1
... ρn) then
This is ensured bymeans that a restriction in Section Interpretationgroup of Formulas . I isa gives meaning to class membership. Itrules is treated as a total function D × D → D .conjunction.
The relationships # and ## are required to havemetadata is ignored for purposes of the usual property that all membersRIF-BLD semantics.
A model of a subclass are also membersgroup of the superclass, i.e., o # cl and cl ## scl must imply o # sclrules, Γ, is a
semantic structure I such that
TValI(Γ) = t. In this case, we
write I |= Γ. ☐
Note that although metadata associated with RIF-BLD formulas is
ensuredignored by the semantics, it can be extracted by XML tools. Since
metadata is represented by frame terms, it can be reasoned with by
RIF-BLD rules.
We now define what it means for a restriction in Section Interpretationset of Formulas . I = gives meaningRIF-BLD rules to the equality. Itentail
a RIF-BLD condition. We say that a RIF-BLD condition formula
φ is existentially closed, if and only if every
variable, ?V, in φ occurs in a total function D × D → Dsubformula of the
form Exists ...?V...(ψ).
I Truth isDefinition
(Logical entailment). Let Γ be a total mapping D → TV .RIF-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 used to define truth valuation of formulas. We also definethe following mapping I :case that TValI (k)(φ)
= t.
Equivalently, we can say that Γ |= φ holds
iff whenever I C (k), if k is a symbol in Const I (?v) = |= Γ it
follows that also I V (?v), if ?v |= φ.
☐
The XML serialization for RIF-BLD is alternating or
fully striped [ANF01]. 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 nfully striped serialization views XML documents as
objects and divides all XML tags into class descriptors, called
type tags, I (v n ) > }) Hereand property descriptors, called role
tags. We use {...} to denotecapitalized names for type tags and lowercase
names for role tags.
XML serialization of the presentation syntax of Section EBNF for RIF-BLD Condition Language uses the following tags.
- And (conjunction) - Or (disjunction) - Exists (quantified formula for 'Exists', containing declare and formula roles) - declare (declare role, containing a Var) - formula (formula role, containing a FORMULA) - Atom (atom formula, positional or with named arguments) - External (external call, containing abagofargument/valuepairs.I(o[a1->v1... ak->vk])=Icontent role) - content (content role, containing an Atom, for predicates, or Expr, for functions) - Member (member formula) - Subclass (subclass formula) - Frame(I(o))({<I((Frame formula) - object (Member/Frame role, containing a1),I(v1)>,...,<I(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 an),I(vn)>})Here{...}denotesProp) - Prop (Property, prefix version of slot infix '->') - key (Prop key role, containing abagConst) - val (Prop val role, containing a TERM) - Equal (prefix version ofattribute/valuepairs.I(c1##c2)=Isub(I(c1),I(c2))I(o#c)=Iisa(I(o),I(c))I(x=y)=I=(I(x),I(y))term equation '=') - Expr (expression formula, positional or with named arguments) - side (Equal left-hand side and right-hand side role) - Const (individual, function, or predicate symbol, with optional 'type' attribute) - Name (name of named argument) - Var (logic variable)
For the effectXML Schema Definition (XSD) of data types.the data types in DTS imposeRIF-BLD condition
language see Appendix XML Schema
for BLD.
The following restrictions. If dt is aXML syntax for symbol space identifier ofspaces utilizes the type
attribute associated with XML term elements such as Const.
For instance, a literal in the xsd:dateTime data type, let LS dt denotetype can
be represented as
<Const type="xsd:dateTime">2007-11-23T03:55:44-02:30</Const>.
Example 4 (A RIF condition and its XML serialization).
This example illustrates XML serialization for RIF conditions.
As before, the lexical space of dt , VS dt denotecompact 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 condition 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=?Author ) XML 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 and its value space,XML serialization).
This example illustrates XML serialization of RIF conditions that involve terms with named arguments.
Compact URI prefixes: bks expands into http://example.com/books# auth expands into http://example.com/authors# cpt expands into http://example.com/concepts# curr expands into http://example.com/currencies#
RIF condition: AndLdt:LSdt→VSdtthelexical-to-value-spacemapping(for(Exists ?Buyer ?P ( ?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 definitions of these concepts, seeRIF-BLD serialization from Section Primitive Data Types of RIF-FLD). ThenXML for RIF-BLD Condition
Language by including rules as described in Section EBNF for RIF-BLD Rule
Language. The extended serialization uses the following
must hold: VS dt ⊆ D ; andadditional tags.
- Group (nested collection of rules annotated with metadata) - meta (meta role, containing metadata, which is represented as a Frame) - rule (rule role, containing RULE) - Forall (quantified formula foreachconstantlit^^dt∈LSdt,IC(lit^^dt)=Ldt(lit).Thatis,ICmustmap'Forall', containing declare and formula roles) - Implies (implication, containing if and then roles) - if (antecedent role, containing FORMULA) - then (consequent role, containing ATOMIC)
The constantsXML Schema Definition of a data type dtRIF-BLD is given in accordance with L dtAppendix
XML Schema for BLD.
Example 6 (Serializing a RIF-BLD does not impose restrictions on I Cgroup annotated with
metadata).
This example shows a serialization for constants inthe lexical spaces that do not correspond to primitive datatypes in DTS . 3.4 Interpretation of Formulas Truth valuationgroup from Example 3.
For well-formed formulas in RIF-BLD is determined usingconvenience, 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 preciselygroup is reproduced at the expected properties, ittop and then is
required that I Truth ( 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] (x = y))=tifandonlyifIForall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays (x"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))) )=IForall ?item (y"cpt:reject"^^rif:iri("ppl:Fred"^^rif:iri ?item) :- "cpt:unsolicited"^^rif:iri(?item) )andthatITruth(I(x = y))=fotherwise.Subclass:TValI(sc ## cl)=ITruth(I(sc ## cl)).XML syntax: <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> <rule> <Forall> <declare><Var>item</Var></declare> <declare><Var>deliverydate</Var></declare> <declare><Var>scheduledate</Var></declare> <declare><Var>diffduration</Var></declare> <declare><Var>diffdays</Var></declare> <formula> <Implies> <if> <And> <formula> <Atom> <op><Const type="rif:iri">cpt:perishable</Const></op> <arg><Var>item</Var></arg> </Atom> </formula> <formula> <Atom> <op><Const type="rif:iri">cpt:delivered</Const></op> <arg><Var>item</Var></arg> <arg><Var>deliverydate</Var></arg> <arg><Const type="rif:iri">ppl:John</Const></arg> </Atom> </formula> <formula> <Atom> <op><Const type="rif:iri">cpt:scheduled</Const></op> <arg><Var>item</Var></arg> <arg><Var>scheduledate</Var></arg> </Atom> </formula> <formula> <External> <content> <Atom> <op><Const type="rif:iri">fn:subtract-dateTimes-yielding-dayTimeDuration</Const></op> <arg><Var>deliverydate</Var></arg> <arg><Var>scheduledate</Var></arg> <arg><Var>diffduration</Var></arg> </Atom> </content> </External> </formula> <formula> <External> <content> <Atom> <op><Const type="rif:iri">fn:get-days-from-dayTimeDuration</Const></op> <arg><Var>diffduration</Var></arg> <arg><Var>diffdays</Var></arg> </Atom> </content> </External> </formula> <formula> <External> <content> <Atom> <op><Const type="rif:iri">op:numeric-greater-than</Const></op> <arg><Var>diffdays</Var></arg> <arg><Const type="xsd:long">10</Const></arg> </Atom> </content> </External> </formula> </And> </if> <then> <Atom> <op><Const type="xsd:long">reject</Const></op> <arg><Const type="rif:iri">ppl:John</Const></arg> <arg><Var>item</Var></arg> </Atom> </then> </Implies> </formula> </Forall> </rule> <rule> <Forall> <declare><Var>item</Var></declare> <formula> <Implies> <if> <Atom> <op><Const type="rif:iri">cpt:unsolicited</Const></op> <arg><Var>item</Var></arg> </Atom> </if> <then> <Atom> <op><Const type="rif:iri">cpt:reject</Const></op> <arg><Const type="rif:iri">ppl:Fred</Const></arg> <arg><Var>item</Var></arg> </Atom> </then> </Implies> </formula> </Forall> </rule> </Group>
We now show how to ensure thattranslate between the operator ##presentation and XML
syntaxes of RIF-BLD.
The translation between the presentation syntax and the XML
syntax of the RIF-BLD Condition Language is transitive, i.e., c1 ## c2 and c2 ## c3 imply c1 ## c3 ,specified by the followingtable
below. Since the presentation syntax of RIF-BLD 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 )).context
sensitive, the translation must differentiate between the terms
that occur in the position of the individuals from terms that occur
as atomic formulas. To ensurethis end, in the translation table, the
positional and named argument terms that all membersoccur in the context of
a subclassatomic formulas are also membersdenoted by the expressions of the superclass, i.e., o # clform
pred(...) 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 ]terms that occur as individuals are
denoted by expressions of the form func(...).
The prime symbol (for instance,
variable') = I Truth ( Iindicates that the
translation function defined by the table must be applied
recursively (i.e., to variable in our example).
Presentation Syntax | XML Syntax |
---|---|
And ( |
<And> <formula>conjunct1 |
Or ( |
<Or> <formula>disjunct1 |
Exists variable1 |
<Exists> <declare>variable1'</declare> . . . <declare>variablen'</declare> <formula>body'</formula> </Exists> |
pred ( |
<Atom> <op>pred'</op> <arg>argument1 |
External ( |
<External> <content>atomexpr'</content> </External> |
func ( |
|
pred ( |
|
func ( |
|
inst [ key1 -> filler1 . |
<Frame> <object>inst'</object> <slot> <Prop> <key>key1 |
inst # class [ key1 -> filler1 . |
<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 = |
<Equal> <side>left'</side> <side>right'</side> </Equal> |
unicode^^space |
<Const type="space">unicode</Const> |
?unicode |
<Var>unicode</Var> |
The translation between the presentation syntax and the XML
syntax of the RIF-BLD Rule Language is given by the case that TVal I (ψ) ≤ TVal I (φ). Equivalently, we can say that R |= φ holds iff whenever I |= R it follows that also I |= φ. 4table below,
which extends the translation table of Section Translation of
RIF-BLD Condition Language.
Presentation Syntax | XML Syntax |
---|---|
Group ( clause1 . . . clausen ) |
<Group> <rule>clause1'</rule> . . . <rule>clausen'</rule> </Group> |
Group metaframe ( clause1 . . . clausen ) |
<Group> <meta>metaframe'</meta> <rule>clause1'</rule> . . . <rule>clausen'</rule> </Group> |
Forall variable1 . . . variablen ( rule ) |
<Forall> <declare>variable1'</declare> . . . <declare>variablen'</declare> <formula>rule'</formula> </Forall> |
conclusion :- condition |
<Implies> <if>condition'</if> <then>conclusion'</then> </Implies> |
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 BLDRIF-BLD sublanguages are available below and
online, with
examples.
<?xmlversion="1.0"encoding="UTF-8"?>version="1.0" encoding="UTF-8"?>
<xs:schemaxmlns: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: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,v0.72008-02-12dhirtle/hboley"><xs:annotation><xs:documentation>0.8 2008-04-07 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:
CONDITIONFORMULA ::= 'And' '('CONDITION*FORMULA* ')' | 'Or' '('CONDITION*FORMULA* ')' | 'Exists' Var+ '('CONDITIONFORMULA ')' |COMPOUNDCOMPOUNDATOMIC | 'External' '(' Atom ')' ATOMIC ::=UnitermAtom | Equal | Member | Subclass | Frame Atom ::= UNITERM UNITERM ::= Const '(' (TERM* |(Const'->'(Name '->' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM'->''->' TERM)* ']' TERM ::= Const | Var |COMPOUNDExpr | 'External' '(' Expr ')' Expr ::= UNITERM Const ::=LITERAL'^^''"' UNICODESTRING '"^^' SYMSPACE Name ::= UNICODESTRING Var ::= '?'VARNAME</xs:documentation></xs:annotation>UNICODESTRING
</xs:documentation> </xs:annotation> <xs:groupname="CONDITION"><!--CONDITION::='And''('CONDITION*')'|'Or''('CONDITION*')'|'Exists'Var+'('CONDITION')'|COMPOUND--><xs:choice>name="FORMULA"> <xs:choice> <xs:elementref="And"/>ref="And"/> <xs:elementref="Or"/>ref="Or"/> <xs:elementref="Exists"/>ref="Exists"/> <xs:groupref="COMPOUND"/></xs:choice></xs:group><xs:elementname="And"><xs:complexType><xs:sequence><xs:elementref="formula"minOccurs="0"maxOccurs="unbounded"/></xs:sequence></xs:complexType></xs:element><xs:elementname="Or"><xs:complexType><xs:sequence><xs:elementref="formula"minOccurs="0"maxOccurs="unbounded"/></xs:sequence></xs:complexType></xs:element><xs:elementname="Exists"><xs:complexType><xs:sequence><xs:elementref="declare"minOccurs="1"maxOccurs="unbounded"/><xs:elementref="formula"/></xs:sequence></xs:complexType></xs:element><xs:elementname="formula"><xs:complexType><xs:sequence>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:groupref="CONDITION"/></xs:sequence></xs:complexType></xs:element><xs:elementname="declare"><xs:complexType><xs:sequence><xs:elementref="Var"/></xs:sequence></xs:complexType></xs:element>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:groupname="COMPOUND"><!--COMPOUND::=Uniterm|Equal|Member|Subclass|Frame--><xs:choice>name="ATOMIC"> <xs:choice> <xs:elementref="Uniterm"/>ref="Atom"/> <xs:elementref="Equal"/>ref="Equal"/> <xs:elementref="Member"/>ref="Member"/> <xs:elementref="Subclass"/>ref="Subclass"/> <xs:elementref="Frame"/></xs:choice></xs:group>ref="Frame"/> </xs:choice> </xs:group> <xs:elementname="Uniterm"><!--Uniterm::=Const'('(TERM*|(Const'->'TERM)*)')'--><xs:complexType><xs:sequence><xs:elementref="op"/><xs:choice><xs:elementref="arg"minOccurs="0"maxOccurs="unbounded"/><xs:elementref="slot"minOccurs="0"maxOccurs="unbounded"/></xs:choice></xs:sequence></xs:complexType></xs:element><xs:elementname="op"><xs:complexType><xs:sequence><xs:elementref="Const"/></xs:sequence></xs:complexType></xs:element><xs:elementname="arg"><xs:complexType><xs:sequence>name="Atom"> <xs:complexType> <xs:sequence> <xs:groupref="TERM"/></xs:sequence></xs:complexType></xs:element><xs:elementname="slot"><xs:complexType><xs:sequence><xs:elementref="Const"/>ref="UNITERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:groupref="TERM"/></xs:sequence></xs:complexType></xs:element>name="UNITERM"> <xs:sequence> <xs:elementname="Equal"><!--Equal::=TERM'='TERM--><xs:complexType><xs:sequence><xs:elementref="side"/><xs:elementref="side"/></xs:sequence></xs:complexType></xs:element><xs:elementname="side"><xs:complexType><xs:sequence><xs:groupref="TERM"/></xs:sequence></xs:complexType></xs:element>ref="op"/> <xs:choice> <xs:elementname="Member"><!--Member::=TERM'#'TERM--><xs:complexType><xs:sequence><xs:elementref="lower"/><xs:elementref="upper"/></xs:sequence></xs:complexType></xs:element>ref="arg" minOccurs="0" maxOccurs="unbounded"/> <xs:element ref="slot" minOccurs="0" maxOccurs="unbounded"/> </xs:choice> </xs:sequence> </xs:group> <xs:element name="op"> <xs:complexType> <xs:sequence> <xs:element ref="Const"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="arg"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element>
<xs:element name="slot"> <xs:complexType> <xs:sequence> <xs:element ref="Prop"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Prop"> <xs:complexType> <xs:sequence> <xs:element ref="key"/> <xs:element ref="val"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="key"> <xs:complexType> <xs:choice> <xs:elementname="Subclass"><!--Subclass::=TERM'##'TERM--><xs:complexType><xs:sequence><xs:elementref="lower"/><xs:elementref="upper"/></xs:sequence></xs:complexType></xs:element><xs:elementname="lower"><xs:complexType><xs:sequence>ref="Name"/> <xs:groupref="TERM"/></xs:sequence></xs:complexType></xs:element><xs:elementname="upper"><xs:complexType><xs:sequence>ref="TERM"/> </xs:choice> </xs:complexType> </xs:element> <xs:element name="val"> <xs:complexType> <xs:sequence> <xs:groupref="TERM"/></xs:sequence></xs:complexType></xs:element><xs:elementname="Frame"><!--Frame::=TERM'['(TERM'->'TERM)*']'--><xs:complexType><xs:sequence><xs:elementref="object"/><xs:elementname="slot"minOccurs="0"maxOccurs="unbounded"><!--notedifferencefromslotinUniterm--><xs:complexType><xs:sequence>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:groupref="TERM"/>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:groupref="TERM"/></xs:sequence></xs:complexType></xs:element></xs:sequence></xs:complexType></xs:element><xs:elementname="object"><xs:complexType><xs:sequence>ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="upper"> <xs:complexType> <xs:sequence> <xs:groupref="TERM"/></xs:sequence></xs:complexType></xs:element>ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Frame"> <xs:complexType> <xs:sequence> <xs:element ref="object"/> <xs:element ref="slot" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element>
<xs:element name="object"> <xs:complexType> <xs:choice> <xs:groupname="TERM"><!--TERM::=Const|Var|COMPOUND--><xs:choice>ref="TERM"/> <xs:elementref="Const"/>ref="Member"/> <xs:elementref="Var"/>name="Subclass"/> </xs:choice> </xs:complexType> </xs:element>
<xs:groupref="COMPOUND"/></xs:choice></xs:group>name="TERM"> <xs:choice> <xs:elementname="Const"><!--Const::=LITERAL'^^'SYMSPACE-->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:complexTypemixed="true"><xs:sequence/>mixed="true"> <xs:sequence/> <xs:attributename="type"type="xs:string"use="required"/></xs:complexType></xs:element><xs:elementname="Var"type="xs:string"><!--Var::='?'VARNAME--></xs:element></xs:schema>5.2name="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>
<?xmlversion="1.0"encoding="UTF-8"?>version="1.0" encoding="UTF-8"?>
<xs:schemaxmlns: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: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,v0.72008-02-12dhirtle/hboley"><xs:annotation><xs:documentation>0.8 2008-04-07 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*RulesetGroup Group ::= 'Group' IRIMETA? '(' (RULE | Group)* ')' IRIMETA ::=RULE*Frame RULE ::= 'Forall' Var+ '('RULECLAUSE ')' | CLAUSE CLAUSE ::= Implies |COMPOUNDATOMIC Implies ::=COMPOUNDATOMIC ':-'CONDITIONFORMULA Note that this is an extension of the syntax for the RIF-BLD Condition Language (BLDCond.xsd).</xs:documentation></xs:annotation><!--TheRuleLanguageincludestheConditionLanguage--></xs:documentation> </xs:annotation>
<xs:includeschemaLocation="BLDCond.xsd"/>schemaLocation="BLDCond.xsd"/>
<xs:elementname="Document"><!--Document::=Ruleset*--><xs:complexType><xs:sequence><xs:elementref="Ruleset"minOccurs="0"maxOccurs="unbounded"/></xs:sequence></xs:complexType></xs:element><xs:elementname="Ruleset"><!--Ruleset::=RULE*--><xs:complexType><xs:sequence><xs:elementref="rule"minOccurs="0"maxOccurs="unbounded"/></xs:sequence></xs:complexType></xs:element><xs:elementname="rule"><xs:complexType><xs:sequence>name="Document"> <xs:complexType> <xs:sequence> <xs:element ref="Group"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Group"> <xs:complexType> <xs:sequence> <xs:element ref="meta" minOccurs="0" maxOccurs="1"/> <xs:sequence> <xs:choice minOccurs="0" maxOccurs="unbounded"> <xs:element ref="rule"/> <xs:element ref="Group"/> </xs:choice> </xs:sequence> </xs:sequence> </xs:complexType> </xs:element>
<xs:element name="meta"> <xs:complexType> <xs:sequence> <xs:groupref="RULE"/></xs:sequence></xs:complexType></xs:element>ref="IRIMETA"/> </xs:sequence> </xs:complexType> </xs:element>
<xs:groupname="RULE"><!--RULE::='Forall'Var+'('RULE')'|Implies|COMPOUND--><xs:choice>name="IRIMETA"> <xs:sequence> <xs:elementref="Forall"/>ref="Frame"/> </xs:sequence> </xs:group>
<xs:element name="rule"> <xs:complexType> <xs:sequence> <xs:group ref="RULE"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="RULE"> <xs:choice> <xs:elementref="Implies"/>ref="Forall"/> <xs:groupref="COMPOUND"/></xs:choice></xs:group><xs:elementname="Forall"><xs:complexType><xs:sequence><xs:elementref="declare"minOccurs="1"maxOccurs="unbounded"/><!--notedifferentfromformulainAnd,OrandExists-->ref="CLAUSE"/> </xs:choice> </xs:group>
<xs:element name="Forall"> <xs:complexType> <xs:sequence> <xs:element ref="declare" minOccurs="1" maxOccurs="unbounded"/> <xs:elementname="formula"><xs:complexType>name="formula"> <xs:complexType> <xs:groupref="RULE"/></xs:complexType></xs:element></xs:sequence></xs:complexType></xs:element>ref="CLAUSE"/> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element>
<xs:group name="CLAUSE"> <xs:choice> <xs:elementname="Implies"><!--Implies::=COMPOUND':-'CONDITION--><xs:complexType><xs:sequence><xs:elementref="if"/><xs:elementref="then"/></xs:sequence></xs:complexType></xs:element><xs:elementname="if"><xs:complexType><xs:sequence>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:groupref="CONDITION"/></xs:sequence></xs:complexType></xs:element><xs:elementname="then"><xs:complexType><xs:sequence>ref="FORMULA"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="then"> <xs:complexType> <xs:sequence> <xs:groupref="COMPOUND"/></xs:sequence></xs:complexType></xs:element></xs:schema>ref="ATOMIC"/> </xs:sequence> </xs:complexType> </xs:element> </xs:schema>