Difference between revisions of "BLD"
Harold Boley (Talk  contribs) 
Harold Boley (Talk  contribs) (→EBNF for the RIFBLD Rule Language) 

(2 intermediate revisions by the same user not shown)  
Line 335:  Line 335:  
Implies ::= ATOMIC ':' FORMULA  Implies ::= ATOMIC ':' FORMULA  
+  {{EdNotetext=The metadata syntax and the approach to rule identification presented in this draft are currently under discussion by the Working Group. Input is welcome. See Issue51}}  
A RIFBLD <tt>Group</tt> is a nested collection of RIFBLD rules annotated with optional metadata, <tt>IRIMETA</tt>, represented as <tt>Frame</tt>s. A <tt>Group</tt> can contain any number of <tt>RULE</tt>s along with any number of nested <tt>Group</tt>s.  A RIFBLD <tt>Group</tt> is a nested collection of RIFBLD rules annotated with optional metadata, <tt>IRIMETA</tt>, represented as <tt>Frame</tt>s. A <tt>Group</tt> can contain any number of <tt>RULE</tt>s along with any number of nested <tt>Group</tt>s.  
Line 700:  Line 701:  
== XML Serialization Syntax for RIFBLD ==  == XML Serialization Syntax for RIFBLD ==  
+  
+  {{EdNotetext=The XML syntax, including the element tags, is being discussed by the Working Group. Input is welcome. See Issue49}}  
Line 1,106:  Line 1,109:  
−  We now show how to translate between the presentation and XML syntaxes of RIFBLD.  +  We now show how to translate between the presentation and XML syntaxes of RIFBLD. 
+  
+  
+  {{  
+  EdNote  text=This XML syntax translation table is expected to be made more formal in future versions of this draft.  
+  }}  
<span id="sectranslationconditionlanguage" class="anchor"></span>  <span id="sectranslationconditionlanguage" class="anchor"></span> 
Revision as of 15:52, 15 April 2008
__NUMBEREDHEADINGS__
 Document title:
 RIF Basic Logic Dialect (Second Edition)
 Editors
 Harold Boley, National Research Council Canada
 Michael Kifer, State University of New York at Stony Brook
 Abstract

This document, developed by the Rule Interchange Format (RIF) Working Group, specifies a basic format that allows logic rules to be exchanged between rulebased systems.
A separate document RIF Data Types and BuiltIns describes data types and builtin functions and predicates.
 Status of this Document
 @@update This is an automatically generated Mediawiki page, made from some sort of W3Cstyle spec.
Copyright © 2008 W3C^{®} (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark and document use rules apply.
Contents
1 Overview
This document develops RIFBLD (the Basic Logic Dialect of the Rule Interchange Format). From a theoretical perspective, RIFBLD corresponds to the language of definite Horn rules (see Horn Logic) with equality and with a standard firstorder semantics. Syntactically, RIFBLD has a number of extensions to support features such as objects and frames as in Flogic [KLW95], internationalized resource identifiers (or IRIs, defined by [RFC3987]) as identifiers for concepts, and XML Schema data types. In addition, the document RIF RDF and OWL Compatibility defines the syntax and semantics of integrated RIFBLD/RDF and RIFBLD/OWL languages. These features make RIFBLD a Webaware 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.
RIFBLD is defined in two different ways  both normative:

As a specialization of the RIF Framework for Logicbased Dialects
(RIFFLD), which is part of the RIF extensibility framework.
This version of the RIFBLD specification is very short and is presented at the end of this document, in Section RIFBLD as a Specialization of the RIF Framework. It is intended for the reader who is familiar with RIFFLD and, therefore, does not need to go through the much longer direct specification of RIFBLD. This version of the specification is also useful for dialect designers, as it is a concrete example of how a nontrivial RIF dialect can be derived from the RIF framework for logic dialects.
 Independently of the RIF framework for logic dialects, for the benefit of those who desire a quicker path to RIFBLD, e.g. as prospective implementers, and are not interested in the extensibility issues. This version of the RIFBLD specification is given first.
Logicbased RIF dialects that extend RIFBLD in accordance with the RIF Framework for Logic Dialects will be specified in other documents by this working group.
Editor's Note: This document is the latest draft of the RIFBLD specification. A number of extensions are planned to support import of RIF documents, the notion of RIF compliance, and a few others. Tool support for RIFBLD is forthcoming.
2 Direct Specification of RIFBLD Syntax
This normative section specifies the syntax of RIFBLD directly, without relying on RIFFLD. We define both a presentation syntax and an XML syntax. The presentation syntax is not intended to be a concrete syntax for RIFBLD. It is defined in mathematical English and is meant to be used in the definitions and examples. This syntax deliberately leaves out details such as the delimiters of the various syntactic components, escape symbols, parenthesizing, precedence of operators, and the like. Since RIF is an interchange format, it uses XML as its concrete syntax.
Editor's Note: A future version of this document might introduce syntactic shortcuts to simplify writing the examples and test cases.
2.1 Alphabet of RIFBLD
Definition (Alphabet). The alphabet of RIFBLD 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, Or, and :
 quantifiers Exists and Forall
 the symbols =, #, ##, >, and External
 the grouping symbol Group
 auxiliary symbols, such as "(", ")", "[", "]", and "^^"
The set of connective symbols, quantifiers, =, etc., is disjoint from Const and Var. The argument names in ArgNames are written as unicode strings that must not start with a question mark, "?". Variables are written as Unicode strings preceded with the symbol "?".
Constants are written as "literal"^^symspace, where literal is a sequence of Unicode characters and symspace is an identifier for a symbol space. Symbol spaces are defined in Section Symbol Spaces of the RIFFLD document.
Editor's Note: 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 RIFFLD.
The symbols =, #, and ## are used in formulas that define equality, class membership, and subclass relationships. The symbol > is used in terms that have named arguments and in frame formulas. The symbol External indicates that an atomic formula or a function term is defined externally (e.g., a builtin).
The symbol Group is used to organize RIFBLD rules into collections and annotate them with metadata. ☐
The language of RIFBLD is the set of formulas constructed using the above alphabet according to the rules given below.
2.2 Terms
RIFBLD supports several kinds of terms: constants and variables, positional terms, terms with named arguments, equality, membership, and subclass atomic formulas, and frame formulas. The word "term" will be used to refer to any of these constructs.
Definition (Term).
 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 simple, positional, or namedargument terms then t(t_{1} ... t_{n}) is a positional term.
 Terms with named arguments. A term with named arguments is of the form t(s_{1}>v_{1} ... s_{n}>v_{n}), where t ∈ Const and v_{1}, ..., v_{n} are simple, positional, or namedargument terms and s_{1}, ..., s_{n} are pairwise distinct symbols from the set ArgNames.
The constant t here represents a predicate or a function; s_{1}, ..., s_{n} represent argument names; and v_{1}, ..., v_{n} represent argument values. The argument names, s_{1}, ..., s_{n}, are required to be pairwise distinct. Terms with named arguments are like positional terms except that the arguments are named and their order is immaterial. Note that a term of the form f() is both positional and with named arguments.
 Equality terms. If t and s are simple, positional, or namedargument 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 simple, positional, or namedargument terms.
 Subclass terms. t##s is a subclass term if t and s are simple, positional, or namedargument 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 simple, positional, or namedargument terms.
 Externally defined terms. If t is a term then External(t) is an externally defined term.
Such terms are used for representing builtin functions and predicates as well as "procedurally attached" terms or predicates, which might exist in various rulebased systems, but are not specified by RIF. ☐
Membership, subclass, and frame terms are used to describe objects and class hierarchies.
2.3 Wellformedness of Terms
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
 individuals.
The symbols in Const that belong to the supported RIF data types are individuals.
Each predicate and function symbol has precisely one arity.
 For positional symbols, an arity is a nonnegative integer that tells how many arguments the symbol can take.
 For symbols that take named arguments, an arity is a set {s_{1} ... s_{k}} of argument names (s_{i} ∈ ArgNames) that are allowed for that symbol.
The arity of a symbol (or whether it is a predicate, a function, or an individual) is not specified in RIFBLD explicitly. Instead, it is inferred as follows. Each constant symbol, p, in a RIFBLD formula (or a set of formulas) may occur in at most one context:
 An individual.
This means that p is a term by itself, which appears inside some other term (positional, with named arguments, in a frame, etc.).
 A function symbol of a particular arity.
This means that p occurs in a term t of the form p(...) and t itself occurs inside some other term.

A predicate symbol of a particular arity.
This means that p occurs in a term t of the form p(...) and t does not occur inside some other term.
The arity of the symbol and its type is determined by its context. If a symbol from Const occurs in more than one context in a set of formulas, the set is not wellformed in RIFBLD.
For a term of the form External(t) to be wellformed, 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 RIFFLD.
Also, if a term of the form External(p(...)) occurs as an atomic formula then p is considered a predicate symbol.
Editor's Note: The definition of external schemas will eventually also appear in the document Data Types and Builtins, so the above reference will be to that document instead of RIFFLD.
A wellformed term is one that occurs in a wellformed set of fomulas.
2.4 Formulas
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 frame terms are also atomic formulas. A formula of the form External(p(...)) is also called an externally defined atomic formula.
Simple terms (constants and variables) are not formulas. Not all atomic formulas are wellformed. A wellformed atomic formula is an atomic formula that is also a wellformed term (see Section Wellformedness of Terms). More general formulas are constructed out of the atomic formulas with the help of logical connectives.
Definition (Wellformed formula). A wellformed formula is a statement that has one of the following forms:
 Atomic: If φ is a wellformed atomic formula then it is also a wellformed formula.
 Conjunction: If φ_{1}, ..., φ_{n}, n ≥ 0, are wellformed formulas then so is And(φ_{1} ... φ_{n}), called a conjunctive formula. As a special case, And() is allowed and is treated as a tautology, i.e., a formula that is always true.
 Disjunction: If φ_{1}, ..., φ_{n}, n ≥ 0, are wellformed formulas then so is Or(φ_{1} ... φ_{n}), called a disjunctive formula. When n=0, we get Or() as a special case; it is treated as a contradiction, i.e., a formula that is always false.
 Existentials: If φ is a wellformed formula and ?V_{1}, ..., ?V_{n} are variables then Exists ?V_{1} ... ?V_{n}(φ) is an existential formula.
Formulas constructed using the above definitions are called RIFBLD conditions. The following defines the notion of a RIFBLD rule.
 Rule implication: If φ is a wellformed atomic formula and ψ is a RIFBLD condition then φ : ψ is a wellformed formula, called rule implication, provided that φ is not externally defined (i.e., does not have the form External(...)).
 Quantified rule: If φ is a rule implication and ?V_{1}, ..., ?V_{n} are variables then Forall ?V_{1} ... ?V_{n}(φ) is a wellformed formula, called quantified rule. It is required that all the free (i.e., nonquantified) variables in φ occur in the prefix Forall ?V_{1} ... ?V_{n}. Quantified rules will also be referred to as RIFBLD rules.

Group: If φ is a frame term and ρ_{1}, ..., ρ_{n} are RIFBLD rules or group formulas (they can be mixed) then Group φ (ρ_{1} ... ρ_{n}) and Group (ρ_{1} ... ρ_{n}) are group formulas.
Group formulas are used to represent sets of rules annotated with metadata. This metadata is specified using an optional frame term φ. Note that some of the ρ_{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 definitions that RIFBLD has a wide variety of syntactic forms for terms and formulas. This provides the infrastructure for exchanging rule languages that support rich collections of syntactic forms. Systems that do not support some of the syntax directly can still support it through syntactic transformations. For instance, disjunctions in the rule body can be eliminated through a standard transformation, such as replacing p : Or(q r) with a pair of rules p : q, p : r. Terms with named arguments can be reduced to positional terms by ordering the arguments by their names and incorporating them into the predicate name. For instance, p(bb>1 aa>2) can be represented as p_aa_bb(2,1).
2.5 EBNF Grammar for the Presentation Syntax of RIFBLD
So far, the syntax of RIFBLD has been specified in mathematical English. Tool developers, however, may prefer EBNF notation, which provides a more succinct overview of the syntax. Several points should be kept in mind regarding this notation.
 The syntax of firstorder logic is not contextfree, so EBNF does not capture the syntax of RIFBLD precisely. For instance, it cannot capture the section on wellformedness conditions, i.e., the requirement that each symbol in RIFBLD can occur in at most one context. As a result, the EBNF grammar defines a strict superset of RIFBLD (not all rules that are derivable using the EBNF grammar are wellformed rules in RIFBLD).
 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 intentionally, since RIF's presentation syntax is used 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 XMLbased, obtained as a refinement and serialization of the EBNF syntax.
 For all the above reasons, the EBNF syntax is not normative.
2.5.1 EBNF for the RIFBLD Condition Language
The Condition Language represents formulas that can be used in the body of RIFBLD rules. The EBNF grammar for a superset of the RIFBLD condition language is as follows.
FORMULA ::= 'And' '(' FORMULA* ')'  'Or' '(' FORMULA* ')'  'Exists' Var+ '(' FORMULA ')'  ATOMIC  'External' '(' ATOMIC ')' 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 SYMSPACE ::= UNICODESTRING
The production rule for the nonterminal 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. RIFBLD conditions permit only existential variables. A RIFBLD 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 RIFBLD presentation syntax does not commit to any particular vocabulary except for using Unicode strings in constant symbols, as names, and for variables (where UNICODESTRING does not start with a special character such as the ?sign). Constant symbols have the form: "UNICODESTRING"^^SYMSPACE, where SYMSPACE is a Unicode string that represents an identifier or an alias of the symbol space of the constant, and UNICODESTRING is a Unicode string from the lexical space of that symbol space. Names are denoted by Unicode character sequences. Variables are denoted by a UNICODESTRING prefixed with a ?sign. Equality, membership, and subclass terms are selfexplanatory. 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 attributevalue pairs. An External(ATOMIC) is a call to an externally defined predicate, equality, membership, subclassing, or frame. Likewise, External(Expr) is a call to an externally defined function.
Example 1 (RIFBLD 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, and 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 RIFBLD 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 (And ("bks:wd2"^^rif:iri#"cpt:book"^^rif:iri "bks:wd2"^^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 (And (?I#"cpt:book"^^rif:iri ?I["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 (And (?I#"cpt:book"^^rif:iri ?I[author>?X ?S>"bks:LeRif"^^rif:iri]))
2.5.2 EBNF for the RIFBLD Rule Language
The presentation syntax for RIFBLD rules extends the syntax in Section EBNF for RIFBLD Condition Language with the following productions.
Group ::= 'Group' IRIMETA? '(' (RULE  Group)* ')' IRIMETA ::= Frame RULE ::= 'Forall' Var+ '(' CLAUSE ')'  CLAUSE CLAUSE ::= Implies  ATOMIC Implies ::= ATOMIC ':' FORMULA
Editor's Note: The metadata syntax and the approach to rule identification presented in this draft are currently under discussion by the Working Group. Input is welcome. See Issue51
A RIFBLD Group is a nested collection of RIFBLD 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 (nonquantified) 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 RIFBLD 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 (RIFBLD rules).
This example shows a business rule borrowed from the document RIF Use Cases and Requirements:

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.
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 yettobedetermined 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:subtractdateTimesyieldingdayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration)) External("fn:getdaysfromdayTimeDuration"^^rif:iri(?diffduration ?diffdays)) External("op:numericgreaterthan"^^rif:iri(?diffdays "10"^^xsd:integer))) ) b. Universalexistential 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:subtractdateTimesyieldingdayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration)) External("fn:getdaysfromdayTimeDuration"^^rif:iri(?diffduration ?diffdays)) External("op:numericgreaterthan"^^rif:iri(?diffdays "10"^^xsd:integer))) ) )
Example 3 (A RIFBLD group annotated with metadata).
This example shows a group formula that consists of two RIFBLD 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>"20080404"^^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:subtractdateTimesyieldingdayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration)) External("fn:getdaysfromdayTimeDuration"^^rif:iri(?diffduration ?diffdays)) External("op:numericgreaterthan"^^rif:iri(?diffdays "10"^^xsd:integer))) ) Forall ?item ( "cpt:reject"^^rif:iri("ppl:Fred"^^rif:iri ?item) : "cpt:unsolicited"^^rif:iri(?item) ) )
3 Direct Specification of RIFBLD Semantics
This normative section specifies the semantics of RIFBLD directly, without relying on RIFFLD.
3.1 Truth Values
The set TV of truth values in RIFBLD consists of just two values, t and f.
3.2 Semantic Structures
The key concept in a modeltheoretic semantics of a logic language is the notion of a semantic structure. The definition, below, is a little bit more general than necessary. This is done in order to better see the connection with the semantics of the RIF framework.
Definition (Semantic structure). A semantic structure, I, is a tuple of the form <TV, DTS, D, D_{ind}, D_{func}, I_{C}, I_{V}, I_{F}, I_{frame}, I_{SF}, I_{sub}, I_{isa}, I_{=}, I_{external}, I_{truth}>. Here D is a nonempty set of elements called the domain of I, and D_{ind}, D_{func} are nonempty subsets of D. D_{ind} is used to interpret the elements of Const, which denote individuals and D_{func} is used to interpret the elements of Const, which 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 RIFFLD for the semantics of data types).
Editor's Note: In the future versions of this document, the above reference will point to the document Data Types and Builtins instead of RIFFLD.
The other components of I are total mappings defined as follows:

I _{C} maps Const to D.
This mapping interprets constant symbols. In addition:
 If a constant, c ∈ Const, denotes an individual then it is required that I_{C}(c) ∈ D_{ind}.
 If c ∈ Const, denotes a function symbol (positional or with named arguments) then it is required that I_{C}(c) ∈ D_{func}.

I_{V} maps Var to D_{ind}.
This mapping interprets variable symbols.
 I_{F} maps D to functions D*_{ind} → D (here D*_{ind} is a set of all sequences of any finite length over the domain D_{ind})
This mapping interprets positional terms. In addition:
 If d ∈ D_{func} then I_{F}(d) must be a function D*_{ind} → D_{ind}.
 This means that when a function symbol is applied to arguments that are individual objects then the result is also an individual object.
 I_{SF} maps D to the set of total functions of the form SetOfFiniteSets(ArgNames × D_{ind}) → D.
This mapping interprets function symbols with named arguments. In addition:
 If d ∈ D_{func} then I_{SF}(d) must be a function SetOfFiniteSets(ArgNames × D_{ind}) → D_{ind}.
 This is analogous to the interpretation of positional terms with two differences:
 Each pair <s,v> ∈ ArgNames × D_{ind} represents an argument/value pair instead of just a value in the case of a positional term.
 The arguments of a term with named arguments constitute a finite set of argument/value pairs rather than a finite ordered sequence of simple elements. So, the order of the arguments does not matter.
 I_{frame} maps D_{ind} to total functions of the form SetOfFiniteBags(D_{ind} × D_{ind}) → D.
This mapping interprets frame terms. An argument, d ∈ D_{ind}, to I_{frame} represent an object and the finite bag {<a1,v1>, ..., <ak,vk>} represents a bag of attributevalue pairs for d. We will see shortly how I_{frame} is used to determine the truth valuation of frame terms.
Bags (multisets) 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 ?C>?D] becomes o[a>b a>b] if variable ?A and ?C are instantiated with the symbol a and ?B, ?D with b.
 I_{sub} gives meaning to the subclass relationship. It is a mapping of the form D_{ind} × D_{ind} → D.
The operator ## is required to be transitive, i.e., c1 ## c2 and c2 ## c3 must imply c1 ## c3. This is ensured by a restriction in Section Interpretation of Formulas.
 I_{isa} gives meaning to class membership. It is a mapping of the form D_{ind} × D_{ind} → D.
The relationships # and ## are required to have the usual property that all members of a subclass are also members of the superclass, i.e., o # cl and cl ## scl must imply o # scl. This is ensured by a restriction in Section Interpretation of Formulas.
 I_{=} is a mapping of the form D_{ind} × D_{ind} → D.
It gives meaning to the equality operator.

I_{truth} is a mapping of the form D → TV.
It is used to define truth valuation for formulas.

I_{external} is a mapping from the coherent set of schemas for externally defined functions to total functions D* → D. For each external schema σ = (?X_{1} ... ?X_{n}; τ) in the coherent set of such schemas associated with the language, I_{external}(σ) is a function of the form D^{n} → D.
For every external schema, σ, associated with the language, I_{external}(σ) 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, I_{external}(σ) is specified in the document Data Types and Builtins so that:
 If σ is a schema of a builtin function then I_{external}(σ) must be the function defined in the aforesaid document.
 If σ is a schema of a builtin predicate then I_{truth} ο (I_{external}(σ)) (the composition of I_{truth} and I_{external}(σ), a truthvalued function) must be as specified in Data Types and Builtins.
For convenience, we also define the following mapping I from terms to D:
 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))

I(External(t)) = I_{externsl}(σ)(I(s_{1}), ..., I(s_{n})), if t is an instance of the external schema σ = (?X_{1} ... ?X_{n}; τ) by substitution ?X_{1}/s_{1} ... ?X_{n}/s_{1}.
Note that, by definition, External(t) is well formed only if t is an instance of an external schema. Furthermore, by the definition of coherent sets of external schemas, t can be an instance of at most one such schema, so I(External(t)) is welldefined.
Here we use {...} to denote a set of argument/value pairs.
Here {...} denotes a bag of attribute/value pairs.
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 lexicaltovaluespace mapping (for the definitions of these concepts, see Section Primitive Data Types of RIFFLD). Then the following must hold:
 VS_{dt} ⊆ D_{ind}; 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}.
RIFBLD does not impose restrictions on I_{C} for constants in the lexical spaces that do not correspond to primitive datatypes in DTS. ☐
3.3 Interpretation of Formulas
Definition (Truth valuation). Truth valuation for wellformed formulas in RIFBLD 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.
 This is tantamount to saying that TVal_{I}(x = y) = t if I(x) = I(y).
 To ensure that equality has precisely the expected properties, it is required that:
 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, if TVal_{I}(c1 ## c2) = TVal_{I}(c2 ## c3) = t then TVal_{I}(c1 ## c3) = t.
 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, if TVal_{I}(o # cl) = TVal_{I}(cl ## scl) = t then TVal_{I}(o # scl) = t.
 Frame: TVal_{I}(o[a_{1}>v_{1} ... a_{k}>v_{k}]) = I_{truth}(I(o[a_{1}>v_{1} ... a_{k}>v_{k}])).
Since the bag of attribute/value pairs represents the conjunctions of all the pairs, the following is required:

TVal_{I}(o[a_{1}>v_{1} ... a_{k}>v_{k}]) = t if and only if TVal_{I}(o[a_{1}>v_{1}]) = ... = TVal_{I}(o[a_{k}>v_{k}]) = t.

Externally defined atomic formula: TVal_{I}(External(t)) = I_{truth}(I_{external}(σ)(I(s_{1}), ..., I(s_{n}))), if t is an atomic formula that is an instance of the external schema σ = (?X_{1} ... ?X_{n}; τ) by substitution ?X_{1}/s_{1} ... ?X_{n}/s_{1}.
Note that, by definition, External(t) is wellformed only if t is an instance of an external schema. Furthermore, by the definition of coherent sets of external schemas, t can be an instance of at most one such schema, so I(External(t)) is welldefined.
 Conjunction: TVal_{I}(And(c_{1} ... c_{n})) = t if and only if TVal_{I}(c_{1}) = ... = TVal_{I}(c_{n}) = t. Otherwise, TVal_{I}(And(c_{1} ... c_{n})) = f.
 Disjunction: TVal_{I}(Or(c_{1} ... c_{n})) = f if and only if TVal_{I}(c_{1}) = ... = TVal_{I}(c_{n}) = f. Otherwise, TVal_{I}(Or(c_{1} ... c_{n})) = t.
 Quantification:
 TVal_{I}(Exists ?v_{1} ... ?v_{n} (φ)) = t if and only if for some I*, described below, TVal_{I*}(φ) = t.
 TVal_{I}(Forall ?v_{1} ... ?v_{n} (φ)) = t if and only if for every I*, described below, TVal_{I*}(φ) = t.
Here I* is a semantic structure of the form <TV, DTS, D, D_{ind}, D_{func}, I_{C}, I*_{V}, I_{F}, I_{frame}, I_{SF}, I_{sub}, I_{isa}, I_{=}, I_{externsl}, I_{truth}>, which is exactly like I, 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}.
 Rule implication:
 TVal_{I}(conclusion : condition) = t, if either TVal_{I}(conclusion)=t or TVal_{I}(condition)=f.
 TVal_{I}(conclusion : condition) = f otherwise.
 Groups of rules:
If Γ is a group formula of the form Group φ (ρ_{1} ... ρ_{n}) or Group (ρ_{1} ... ρ_{n}) then
 TVal_{I}(Γ) = t if and only if TVal_{I}(ρ_{1}) = t, ..., TVal_{I}(ρ_{n}) = t.
 TVal_{I}(Γ) = f otherwise.
This means that a group of rules is treated as a conjunction. The metadata is ignored for purposes of the RIFBLD semantics.
The empty conjunction is treated as a tautology, so TVal_{I}(And()) = t.
The empty disjunction is treated as a contradiction, so TVal_{I}(Or()) = f.
A model of a group of rules, Γ, is a semantic structure I such that TVal_{I}(Γ) = t. In this case, we write I = Γ. ☐
Note that although metadata associated with RIFBLD formulas is ignored by the semantics, it can be extracted by XML tools. Since metadata is represented by frame terms, it can be reasoned with by RIFBLD rules.
3.4 Logical Entailment
We now define what it means for a set of RIFBLD rules to entail a RIFBLD condition. We say that a RIFBLD condition formula φ is existentially closed, if and only if every variable, ?V, in φ occurs in a subformula of the form Exists ...?V...(ψ).
Definition (Logical entailment). Let Γ be a RIFBLD group formula and φ an existentially closed RIFBLD condition formula. We say that Γ entails φ, written as Γ = φ, if and only if for every model of Γ it is the case that TVal_{I}(φ) = t.
Equivalently, we can say that Γ = φ holds iff whenever I = Γ it follows that also I = φ. ☐
4 XML Serialization Syntax for RIFBLD
Editor's Note: The XML syntax, including the element tags, is being discussed by the Working Group. Input is welcome. See Issue49
The XML serialization for RIFBLD is alternating or fully striped [ANF01]. A fully striped serialization views XML documents as objects and divides all XML tags into class descriptors, called type tags, and property descriptors, called role tags. We use capitalized names for type tags and lowercase names for role tags.
4.1 XML for the RIFBLD Condition Language
XML serialization of the presentation syntax of Section EBNF for RIFBLD Condition Language uses the following tags.
 And (conjunction)  Or (disjunction)  Exists (quantified formula for 'Exists', containing declare and formula roles)  declare (declare role, containing a Var)  formula (formula role, containing a FORMULA)  Atom (atom formula, positional or with named arguments)  External (external call, containing a content role)  content (content role, containing an Atom, for predicates, or Expr, for functions)  Member (member formula)  Subclass (subclass formula)  Frame (Frame formula)  object (Member/Frame role, containing a TERM or an object description)  op (Atom/Expr role for predicates/functions as operations)  arg (positional argument role)  upper (Member/Subclass upper class role)  lower (Member/Subclass lower instance/class role)  slot (Atom/Expr/Frame slot role, containing a Prop)  Prop (Property, prefix version of slot infix '>')  key (Prop key role, containing a Const)  val (Prop val role, containing a TERM)  Equal (prefix version of term equation '=')  Expr (expression formula, positional or with named arguments)  side (Equal lefthand side and righthand side role)  Const (individual, function, or predicate symbol, with optional 'type' attribute)  Name (name of named argument)  Var (logic variable)
For the XML Schema Definition (XSD) of the RIFBLD condition language see Appendix XML Schema for BLD.
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">20071123T03:55:4402:30</Const>.
Example 4 (A RIF condition and its XML serialization).
This example illustrates XML serialization for RIF conditions. As before, the compact URI notation is used for better readability.
Compact URI prefixes: bks expands into http://example.com/books# cpt expands into http://example.com/concepts# curr expands into http://example.com/currencies#
RIF 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 with named arguments and its XML serialization).
This example illustrates XML serialization of RIF conditions that involve terms with named arguments.
Compact URI prefixes: bks expands into http://example.com/books# auth expands into http://example.com/authors# cpt expands into http://example.com/concepts# curr expands into http://example.com/currencies#
RIF condition: And (Exists ?Buyer ?P ( And (?P#"cpt:purchase"^^rif:iri ?P["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> <And> <formula> <Member> <lower><Var>P</Var></lower> <upper><Const type="rif:iri">cpt:purchase</Const></upper> </Member> </formula> <formula> <Frame> <object> <Var>P</Var> </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> </And> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And>
4.2 XML for the RIFBLD Rule Language
We now extend the RIFBLD serialization from Section XML for RIFBLD Condition Language by including rules as described in Section EBNF for RIFBLD Rule Language. The extended serialization uses the following additional tags.
 Group (nested collection of sentences annotated with metadata)  meta (meta role, containing metadata, which is represented as a Frame)  sentence (sentence role, containing RULE or Group)  Forall (quantified formula for 'Forall', containing declare and formula roles)  Implies (implication, containing if and then roles)  if (antecedent role, containing FORMULA)  then (consequent role, containing ATOMIC)
The XML Schema Definition of RIFBLD is given in Appendix XML Schema for BLD.
Example 6 (Serializing a RIFBLD group annotated with metadata).
This example shows a serialization for the group from Example 3. For convenience, the group is reproduced at the top and then is followed by its serialization.
Compact URI prefixes: bks expands into http://example.com/books# auth expands into http://example.com/authors# cpt expands into http://example.com/concepts# dc expands into http://dublincore.org/documents/dces/ w3 expands into http://www.w3.org/
Presentation syntax: Group "http://sample.org"^^rif:iri["dc:publisher"^^rif:iri>"w3:W3C"^^rif:iri "dc:date"^^rif:iri>"20080404"^^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:subtractdateTimesyieldingdayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration)) External("fn:getdaysfromdayTimeDuration"^^rif:iri(?diffduration ?diffdays)) External("op:numericgreaterthan"^^rif:iri(?diffdays "10"^^xsd:integer))) ) Forall ?item ( "cpt:reject"^^rif:iri("ppl:Fred"^^rif:iri ?item) : "cpt:unsolicited"^^rif:iri(?item) ) ) 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">20080404</Const></val> </Prop> </slot> </Frame> </meta> <sentence> <Forall> <declare><Var>item</Var></declare> <declare><Var>deliverydate</Var></declare> <declare><Var>scheduledate</Var></declare> <declare><Var>diffduration</Var></declare> <declare><Var>diffdays</Var></declare> <formula> <Implies> <if> <And> <formula> <Atom> <op><Const type="rif:iri">cpt:perishable</Const></op> <arg><Var>item</Var></arg> </Atom> </formula> <formula> <Atom> <op><Const type="rif:iri">cpt:delivered</Const></op> <arg><Var>item</Var></arg> <arg><Var>deliverydate</Var></arg> <arg><Const type="rif:iri">ppl:John</Const></arg> </Atom> </formula> <formula> <Atom> <op><Const type="rif:iri">cpt:scheduled</Const></op> <arg><Var>item</Var></arg> <arg><Var>scheduledate</Var></arg> </Atom> </formula> <formula> <External> <content> <Atom> <op><Const type="rif:iri">fn:subtractdateTimesyieldingdayTimeDuration</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:getdaysfromdayTimeDuration</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:numericgreaterthan</Const></op> <arg><Var>diffdays</Var></arg> <arg><Const type="xsd:long">10</Const></arg> </Atom> </content> </External> </formula> </And> </if> <then> <Atom> <op><Const type="xsd:long">reject</Const></op> <arg><Const type="rif:iri">ppl:John</Const></arg> <arg><Var>item</Var></arg> </Atom> </then> </Implies> </formula> </Forall> </sentence> <sentence> <Forall> <declare><Var>item</Var></declare> <formula> <Implies> <if> <Atom> <op><Const type="rif:iri">cpt:unsolicited</Const></op> <arg><Var>item</Var></arg> </Atom> </if> <then> <Atom> <op><Const type="rif:iri">cpt:reject</Const></op> <arg><Const type="rif:iri">ppl:Fred</Const></arg> <arg><Var>item</Var></arg> </Atom> </then> </Implies> </formula> </Forall> </sentence> </Group>
4.3 Translation Between the RIFBLD Presentation and XML Syntaxes
We now show how to translate between the presentation and XML syntaxes of RIFBLD.
Editor's Note: This XML syntax translation table is expected to be made more formal in future versions of this draft.
4.3.1 Translation of the RIFBLD Condition Language
The translation between the presentation syntax and the XML syntax of the RIFBLD Condition Language is specified by the table below. Since the presentation syntax of RIFBLD is 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 this end, in the translation table, the positional and named argument terms that occur in the context of atomic formulas are denoted by the expressions of the form pred(...) and the terms that occur as individuals are denoted by expressions of the form func(...).
The prime symbol (for instance, variable') indicates that the translation function defined by the table must be applied recursively (i.e., to variable in our example).
Presentation Syntax  XML 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> 
pred ( argument_{1} . . . argument_{n} ) 
<Atom> <op>pred'</op> <arg>argument_{1}'</arg> . . . <arg> argument_{n}'</arg> </Atom> 
External ( atomexpr ) 
<External> <content>atomexpr'</content> </External> 
func ( argument_{1} . . . argument_{n} ) 
<Expr> <op>func'</op> <arg>argument_{1}'</arg> . . . <arg> argument_{n}'</arg> </Expr> 
pred ( unicodestring_{1} > filler_{1} . . . unicodestring_{n} > filler_{n} ) 
<Atom> <op>pred'</op> <slot> <Prop> <key><Name>unicodestring_{1}</Name></key> <val>filler_{1}'</val> </Prop> </slot> . . . <slot> <Prop> <key><Name>unicodestring_{n}</Name></key> <val>filler_{n}'</val> </Prop> </slot> </Atom> 
func ( unicodestring_{1} > filler_{1} . . . unicodestring_{n} > filler_{n} ) 
<Expr> <op>func'</op> <slot> <Prop> <key><Name>unicodestring_{1}</Name></key> <val>filler_{1}'</val> </Prop> </slot> . . . <slot> <Prop> <key><Name>unicodestring_{n}</Name></key> <val>filler_{n}'</val> </Prop> </slot> </Expr> 
inst [ key_{1} > filler_{1} . . . key_{n} > filler_{n} ] 
<Frame> <object>inst'</object> <slot> <Prop> <key>key_{1}'</key> <val>filler_{1}'</val> </Prop> </slot> . . . <slot> <Prop> <key>key_{n}'</key> <val>filler_{n}'</val> </Prop> </slot> </Frame> 
inst # class 
<Member> <lower>inst'</lower> <upper>class'</upper> </Member> 
sub ## super 
<Subclass> <lower>sub'</lower> <upper>super'</upper> </Subclass> 
left = right 
<Equal> <side>left'</side> <side>right'</side> </Equal> 
unicodestring^^space 
<Const type="space">unicodestring</Const> 
?unicodestring 
<Var>unicodestring</Var> 
4.3.2 Translation of the RIFBLD Rule Language
The translation between the presentation syntax and the XML syntax of the RIFBLD Rule Language is given by the table below, which extends the translation table of Section Translation of RIFBLD Condition Language.
Presentation Syntax  XML Syntax 

Group ( clause_{1} . . . clause_{n} ) 
<Group> <sentence>clause_{1}'</sentence> . . . <sentence>clause_{n}'</sentence> </Group> 
Group metaframe ( clause_{1} . . . clause_{n} ) 
<Group> <meta>metaframe'</meta> <sentence>clause_{1}'</sentence> . . . <sentence>clause_{n}'</sentence> </Group> 
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> 
5 RIFBLD as a Specialization of the RIF Framework
This normative section describes RIFBLD by specializing RIFFLD. The reader is assumed to be familiar with RIFFLD as described in RIF Framework for LogicBased Dialects. The reader who is not interested in how RIFBLD is derived from the framework can skip this section.
5.1 The Syntax of RIFBLD as a Specialization of RIFFLD
This section defines the precise relationship between the syntax of RIFBLD and the syntactic framework of RIFFLD.
The syntax of the RIF Basic Logic Dialect is defined by specialization from the syntax of the RIF Syntactic Framework for Logic Dialects. Section Syntax of a RIF Dialect as a Specialization of the RIF Framework in that document lists the parameters of the syntactic framework in mathematical English, which we will now specialize for RIFBLD.
 Alphabet.
 Assignment of signatures to each constant and variable symbol.
 Basic.
 individual{ }
 atomic{ }
 For every integer n ≥ 0, there are signatures
 f_{n}{(individual ... individual) ⇒ individual}  for nary function symbols,
 p_{n}{(individual ... individual) ⇒ atomic}  for nary predicates.
 For every set of symbols s1,...,sk ∈ ArgNames, there are signatures f_{s1...sk}{(s1>individual ... sk>individual) ⇒ individual} and p_{s1...sk}{(s1>individual ... sk>individual) ⇒ atomic}. These are signatures for terms and predicates with arguments named s1, ..., sk, respectively. In this specialization of RIFFLD, the argument names s1, ..., sk must be pairwise distinct.
 A symbol in Const can have exactly one signature, individual, f_{n}, or p_{n}, where n ≥ 0, or f_{s1...sk}{(s1>individual ... sk>individual) ⇒ individual}, p_{s1...sk}{(s1>individual ... sk>individual) ⇒ atomic}, for some s1,...,sk ∈ ArgNames. It cannot have the signature atomic, since only complex terms can have such signatures. Thus, by itself a symbol cannot be a proposition in RIFBLD, but a term of the form p() can be.
Thus, in RIFBLD each constant symbol can be either an individual, a function of one particular arity or with certain argument names, a predicate of one particular arity or with certain argument names, an externally defined function of one particular arity, or an externally defined predicate symbol of one particular arity  it is not possible for the same symbol to play more than one role.
 The constant symbols that belong to the supported RIF data types (XML Schema data types, rdf:XMLLiteral, rif:text) all have the signature individual in RIFBLD.
 The symbols of type rif:iri and rif:local can have the following signatures in RIFBLD: individual, f_{n}, or p_{n}, for n = 0,1,....; or f_{s1...sk}, p_{s1...sk}, for some argument names s1,...,sk ∈ ArgNames.
 All variables are associated with signature individual{ }, so they can range only over individuals.
 The signature for equality is ={(individual individual) ⇒ atomic}.
This means that equality can compare only those terms whose signature is individual; it cannot compare predicate names or function symbols. Equality 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.
 The frame signature, >, is >{(individual individual individual) ⇒ atomic}.
Note that this precludes the possibility that a frame term might occur as an argument to a predicate, a function, or inside some other term.
 The membership signature, #, is #{(individual individual) ⇒ atomic}.
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.
 The signature for the subclass relationship is ##{(individual individual) ⇒ atomic}.
As with frames and membership terms, this precludes the possibility that a subclass term might occur inside some other term.
 Supported types of terms.
 RIFBLD supports all the term types defined by the syntactic framework (see the Section Terms of RIFFLD):
 constants
 variables
 positional
 with named arguments
 equality
 frame
 membership
 subclass
 external
 Compared to RIFFLD, terms (both positional and with named arguments) have significant restrictions. This is so in order to give BLD a relatively compact nature.
 The signature for the variable symbols does not permit them to occur in the context of predicates, functions, or formulas. In particular, in the RIFBLD specialization of RIFFLD, a variable is not an atomic formula.
 Likewise, a symbol cannot be an atomic formula by itself. That is, if p ∈ Const then p is not a wellformed 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, RIFBLD signatures ensure that all variables have the signature individual{ } and all other terms, except for the constants from Const, can have either the signature individual{ } or atomic{ }. Therefore, if t is a (nonConst) term then t(...) is not a wellformed term.
 Supported symbol spaces.
 xsd:string
 xsd:decimal
 xsd:time
 xsd:date
 xsd:dateTime
 rdf:XMLLiteral
 rif:text
 rif:iri
 rif:local
 Supported formulas.
 RIFBLD condition
 RIFBLD rule
 The head (or conclusion) of the rule is an atomic formula, which is not an externally defined predicate (i.e., it cannot have the form External(...)).
 The body (or premise) of the rule is a RIFBLD condition.
 All free (nonquantified) variables in the rule must be quantified with Forall outside of the rule (i.e., Forall ?vars (head : body)).

RIFBLD group
A RIFBLD group is a RIFFLD group that contains only RIFBLD rules and RIFBLD groups.

The alphabet of RIFBLD is the alphabet of RIFFLD with the negation
symbols Neg and Naf excluded.
The signature set of RIFBLD contains the following signatures:
The signature individual{ } represents the context in which individual objects (but not atomic formulas) can appear.
The signature atomic{ } represents the context where atomic formulas can occur.
These represent function and predicate symbols of arity n (each of the above cases has n individuals as arguments inside the parentheses).
RIFBLD uses no special syntax for declaring signatures. Instead, the author specifies signatures contextually. That is, since RIFBLD requires that each symbol is associated with a unique signature, the signature is determined from the context in which the symbol is used. If a symbol is used in more than one context, the parser must treat this as a syntax error. If no errors are found, all terms and atomic formulas are guaranteed to be wellformed. Thus, signatures are not part of the RIFBLD language, and individual and atomic are not reserved keywords in RIFBLD.
RIFBLD supports all the symbol spaces defined in Section Symbol Spaces of the syntactic framework:
RIFBLD supports the following types of formulas (see Wellformed Terms and Formulas for the definitions):
A RIFBLD condition is an atomic formula, a conjunctive or disjunctive combination of atomic formulas with optional existential quantification of variables, or an external atomic formula.
A RIFBLD rule is a universally quantified RIFFLD rule with the following restrictions:
Recall that negation (classical or default) is not supported by RIFBLD in either the rule head or the body.
Editor's Note: The list of supported symbol spaces will move to another document, Data Types and BuiltIns. Any existing discrepancies will be fixed at that time.
5.2 The Semantics of RIFBLD as a Specialization of RIFFLD
This normative section defines the precise relationship between the semantics of RIFBLD and the semantic framework of RIFFLD. Specification of the semantics that does not rely on RIFFLD is given in Section Direct Specification of RIFBLD Semantics.
The semantics of the RIF Basic Logic Dialect is defined by specialization from the semantics of the Semantic Framework for Logic Dialects of RIF. Section Semantics of a RIF Dialect as a Specialization of the RIF Framework in that document lists the parameters of the semantic framework, which one need to specialize. Thus, for RIFBLD, we need to look at the following parameters:
 The effect of the syntax.
 Truth values.
 Data types.
 xsd:long
 xsd:integer
 xsd:decimal
 xsd:string
 xsd:time
 xsd:dateTime
 rdf:XMLLiteral
 rif:text
 Logical entailment.
 as a set of all models; or
 as the unique minimal model.
RIFBLD does not support negation. This is the only obvious simplification with respect to RIFFLD as far as the semantics is concerned. The restrictions on the signatures of symbols in RIFBLD do not affect the semantics in a significant way.
The set TV of truth values in RIFBLD consists of just two values, t and f such that f <_{t} t. The order <_{t} is total.
RIFBLD supports all the data types listed in Section Primitive Data Types of RIFFLD:
Recall that logical entailment in RIFFLD is defined with respect to an unspecified set of intended semantic structures and that dialects of RIF must make this notion concrete. For RIFBLD, this set is defined in one of the two following equivalent ways:
These two definitions are equivalent for entailment of existentially closed RIFBLD conditions by RIFBLD sets of formulas, since all rules in RIFBLD are Horn  it is a classical result of Van Emden and Kowalski [vEK76].
Editor's Note: The list of supported data types will move to another document, Data Types and BuiltIns. Any existing discrepancies will be fixed at that time.
6 References
6.1 Normative References
 [RDFCONCEPTS]
 Resource Description Framework (RDF): Concepts and Abstract Syntax, Klyne G., Carroll J. (Editors), W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/RECrdfconcepts20040210/. Latest version available at http://www.w3.org/TR/rdfconcepts/.
 [RDFSEMANTICS]
 RDF Semantics, Patrick Hayes, Editor, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/RECrdfmt20040210/. Latest version available at http://www.w3.org/TR/rdfmt/.
 [RDFSCHEMA]
 RDF Vocabulary Description Language 1.0: RDF Schema, Brian McBride, Editor, W3C Recommendation 10 February 2004, http://www.w3.org/TR/rdfschema/.
 [RFC3066]
 RFC 3066  Tags for the Identification of Languages, H. Alvestrand, IETF, January 2001. This document is http://www.isi.edu/innotes/rfc3066.txt.
 [RFC3987]
 RFC 3987  Internationalized Resource Identifiers (IRIs), M. Duerst and M. Suignard, IETF, January 2005. This document is http://www.ietf.org/rfc/rfc3987.txt.
 [XMLSCHEMA2]
 XML Schema Part 2: Datatypes, W3C Recommendation, World Wide Web Consortium, 2 May 2001. This version is http://www.w3.org/TR/2001/RECxmlschema220010502/. The latest version is available at http://www.w3.org/TR/xmlschema2/.
6.2 Informational References
 [ANF01]
 Normal Form Conventions for XML Representations of Structured Data, Henry S. Thompson. October 2001.
 [KLW95]
 Logical foundations of objectoriented and framebased languages, M. Kifer, G. Lausen, J. Wu. Journal of ACM, July 1995, pp. 741843.
 [CKW93]
 HiLog: A Foundation for higherorder logic programming, W. Chen, M. Kifer, D.S. Warren. Journal of Logic Programming, vol. 15, no. 3, February 1993, pp. 187230.
 [CK95]
 Sorted HiLog: Sorts in HigherOrder 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. 252265.
 [RDFSYN04]
 RDF/XML Syntax Specification (Revised), Dave Beckett, Editor, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/RECrdfsyntaxgrammar20040210/. Latest version available at http://www.w3.org/TR/rdfsyntaxgrammar/.
 [Shoham87]
 Nonmonotonic logics: meaning and utility, Y. Shoham. Proc. 10th International Joint Conference on Artificial Intelligence, Morgan Kaufmann, pp. 388393, 1987.
 [CURIE]
 CURIE Syntax 1.0: A compact syntax for expressing URIs, Mark Birbeck. Draft, 2005. Available at http://www.w3.org/2001/sw/BestPractices/HTML/20051027CURIE.
 [CycL]
 The Syntax of CycL, Web site. Available at http://www.cyc.com/cycdoc/ref/cyclsyntax.html.
 [FL2]
 FLORA2: An ObjectOriented Knowledge Base Language, M. Kifer. Web site. Available at http://flora.sourceforge.net.
 [OOjD]
 ObjectOriented jDREW, Web site. Available at http://www.jdrew.org/oojdrew/.
 [GRS91]
 The WellFounded Semantics for General Logic Programs, A. Van Gelder, K.A. Ross, J.S. Schlipf. Journal of ACM, 38:3, pages 620650, 1991.
 [GL88]
 The Stable Model Semantics for Logic Programming, M. Gelfond and V. Lifschitz. Logic Programming: Proceedings of the Fifth Conference and Symposium, pages 10701080, 1988.
 [vEK76]
 The semantics of predicate logic as a programming language, M. van Emden and R. Kowalski. Journal of the ACM 23 (1976), 733742.
7 Appendix: Subdialects of RIFBLD
The following is a proposal, under discussion, for specifying RIFCORE and some other subdialects of BLD by removing certain syntactic constructs from RIFBLD and the corresponding restrictions on the semantics (hence, by further specializing RIFBLD). For some engines it might be preferable or more natural to support only some subdialects of RIFBLD. These subdialects of BLD can also be reused in the definitions of other RIF dialects.
The syntactic structure of RIFBLD suggests several useful subdialects:
 RIFCORE. This subdialect is obtained from RIFBLD by removing support for:
 equality formulas in the rule conclusions (while still allowing them in conditions)
 terms with named arguments
 membership, subclass, and frame terms
 RIFCORE+equality.
 This subdialect extends RIFCORE by adding support for equality formulas in the rule conclusions.
 RIFCORE+named arguments.
 This subdialect extends RIFCORE by adding syntactic support for terms with named arguments.
8 Appendix: XML Schema for RIFBLD
The namespace of RIF is http://www.w3.org/2007/rif#.
XML schemas for the RIFBLD sublanguages are available below and online, with examples.
8.1 Condition Language
<?xml version="1.0" encoding="UTF8"?> <xs:schema xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns="http://www.w3.org/2007/rif#" targetNamespace="http://www.w3.org/2007/rif#" elementFormDefault="qualified" version="Id: BLDCond.xsd,v 0.8 20080414 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 RIFBLD Condition Language: FORMULA ::= 'And' '(' FORMULA* ')'  'Or' '(' FORMULA* ')'  'Exists' Var+ '(' FORMULA ')'  ATOMIC  'External' '(' ATOMIC ')' ATOMIC ::= Atom  Equal  Member  Subclass  Frame Atom ::= UNITERM UNITERM ::= Const '(' (TERM*  (Name '>' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '>' TERM)* ']' TERM ::= Const  Var  Expr  'External' '(' Expr ')' Expr ::= UNITERM Const ::= '"' UNICODESTRING '"^^' SYMSPACE Name ::= UNICODESTRING Var ::= '?' UNICODESTRING </xs:documentation> </xs:annotation> <xs:group name="FORMULA"> <xs:choice> <xs:element ref="And"/> <xs:element ref="Or"/> <xs:element ref="Exists"/> <xs:group ref="ATOMIC"/> <xs:element name="External" type="ExternalFORMULA.type"/> </xs:choice> </xs:group> <xs:complexType name="ExternalFORMULA.type"> <xs:sequence> <xs:element name="content" type="contentFORMULA.type"/> </xs:sequence> </xs:complexType> <xs:complexType name="contentFORMULA.type"> <xs:sequence> <xs:group ref="ATOMIC"/> </xs:sequence> </xs:complexType> <xs:element name="And"> <xs:complexType> <xs:sequence> <xs:element ref="formula" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Or"> <xs:complexType> <xs:sequence> <xs:element ref="formula" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Exists"> <xs:complexType> <xs:sequence> <xs:element ref="declare" minOccurs="1" maxOccurs="unbounded"/> <xs:element ref="formula"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="formula"> <xs:complexType> <xs:sequence> <xs:group ref="FORMULA"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="declare"> <xs:complexType> <xs:sequence> <xs:element ref="Var"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="ATOMIC"> <xs:choice> <xs:element ref="Atom"/> <xs:element ref="Equal"/> <xs:element ref="Member"/> <xs:element ref="Subclass"/> <xs:element ref="Frame"/> </xs:choice> </xs:group> <xs:element name="Atom"> <xs:complexType> <xs:sequence> <xs:group ref="UNITERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="UNITERM"> <xs:sequence> <xs:element ref="op"/> <xs:choice> <xs:element ref="arg" minOccurs="0" maxOccurs="unbounded"/> <xs:element name="slot" type="slotUNITERM.type" minOccurs="0" maxOccurs="unbounded"/> </xs:choice> </xs:sequence> </xs:group> <xs:element name="op"> <xs:complexType> <xs:sequence> <xs:element ref="Const"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="arg"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:complexType name="slotUNITERM.type"> <xs:sequence> <xs:element name="Prop" type="PropUNITERM.type"/> </xs:sequence> </xs:complexType> <xs:complexType name="PropUNITERM.type"> <xs:sequence> <xs:element name="key" type="keyUNITERM.type"/> <xs:element ref="val"/> </xs:sequence> </xs:complexType> <xs:complexType name="keyUNITERM.type"> <xs:sequence> <xs:element ref="Name"/> </xs:sequence> </xs:complexType> <xs:element name="val"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Equal"> <xs:complexType> <xs:sequence> <xs:element ref="side"/> <xs:element ref="side"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="side"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Member"> <xs:complexType> <xs:sequence> <xs:element ref="lower"/> <xs:element ref="upper"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Subclass"> <xs:complexType> <xs:sequence> <xs:element ref="lower"/> <xs:element ref="upper"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="lower"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="upper"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Frame"> <xs:complexType> <xs:sequence> <xs:element ref="object"/> <xs:element name="slot" type="slotFrame.type" minOccurs="0" maxOccurs="unbounded"/> </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:complexType name="slotFrame.type"> <xs:sequence> <xs:element name="Prop" type="PropFrame.type"/> </xs:sequence> </xs:complexType> <xs:complexType name="PropFrame.type"> <xs:sequence> <xs:element name="key" type="keyFrame.type"/> <xs:element ref="val"/> </xs:sequence> </xs:complexType> <xs:complexType name="keyFrame.type"> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> <xs:group name="TERM"> <xs:choice> <xs:element ref="Const"/> <xs:element ref="Var"/> <xs:element ref="Expr"/> <xs:element name="External" type="ExternalTERM.type"/> </xs:choice> </xs:group> <xs:complexType name="ExternalTERM.type"> <xs:sequence> <xs:element name="content" type="contentTERM.type"/> </xs:sequence> </xs:complexType> <xs:complexType name="contentTERM.type"> <xs:sequence> <xs:element ref="Expr"/> </xs:sequence> </xs:complexType> <xs:element name="Expr"> <xs:complexType> <xs:sequence> <xs:group ref="UNITERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Const"> <xs:complexType mixed="true"> <xs:sequence/> <xs:attribute name="type" type="xs:string" use="required"/> </xs:complexType> </xs:element> <xs:element name="Name" type="xs:string"> </xs:element> <xs:element name="Var" type="xs:string"> </xs:element> </xs:schema>
8.2 Rule Language
<?xml version="1.0" encoding="UTF8"?> <xs:schema xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns="http://www.w3.org/2007/rif#" targetNamespace="http://www.w3.org/2007/rif#" elementFormDefault="qualified" version="Id: BLDRule.xsd,v 0.8 20080409 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 RIFBLD Rule Language: Document ::= Group Group ::= 'Group' IRIMETA? '(' (RULE  Group)* ')' IRIMETA ::= Frame RULE ::= 'Forall' Var+ '(' CLAUSE ')'  CLAUSE CLAUSE ::= Implies  ATOMIC Implies ::= ATOMIC ':' FORMULA Note that this is an extension of the syntax for the RIFBLD Condition Language (BLDCond.xsd). </xs:documentation> </xs:annotation> <xs:include schemaLocation="BLDCond.xsd"/> <xs:element name="Document"> <xs:complexType> <xs:sequence> <xs:element ref="Group"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Group"> <xs:complexType> <xs:sequence> <xs:element ref="meta" minOccurs="0" maxOccurs="1"/> <xs:element ref="sentence" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="meta"> <xs:complexType> <xs:sequence> <xs:group ref="IRIMETA"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="IRIMETA"> <xs:sequence> <xs:element ref="Frame"/> </xs:sequence> </xs:group> <xs:element name="sentence"> <xs:complexType> <xs:choice> <xs:element ref="Group"/> <xs:group ref="RULE"/> </xs:choice> </xs:complexType> </xs:element> <xs:group name="RULE"> <xs:choice> <xs:element ref="Forall"/> <xs:group ref="CLAUSE"/> </xs:choice> </xs:group> <xs:element name="Forall"> <xs:complexType> <xs:sequence> <xs:element ref="declare" minOccurs="1" maxOccurs="unbounded"/> <xs:element name="formula"> <xs:complexType> <xs:group ref="CLAUSE"/> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="CLAUSE"> <xs:choice> <xs:element ref="Implies"/> <xs:group ref="ATOMIC"/> </xs:choice> </xs:group> <xs:element name="Implies"> <xs:complexType> <xs:sequence> <xs:element ref="if"/> <xs:element ref="then"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="if"> <xs:complexType> <xs:sequence> <xs:group ref="FORMULA"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="then"> <xs:complexType> <xs:sequence> <xs:group ref="ATOMIC"/> </xs:sequence> </xs:complexType> </xs:element> </xs:schema>