Difference between revisions of "BLD"
JosDeBruijn (Talk  contribs) (→Formulas: including anchor for conditions) 
Harold Boley (Talk  contribs) (→EBNF for RIFBLD Condition Language) 

(2 intermediate revisions by the same user not shown)  
Line 273:  Line 273:  
'Or' '(' CONDITION* ')'   'Or' '(' CONDITION* ')'   
'Exists' Var+ '(' CONDITION ')'   'Exists' Var+ '(' CONDITION ')'   
−  +  ATOMIC  
−  +  ATOMIC ::= Uniterm  Unicall  Equal  Member  Subclass  Frame  
Uniterm ::= Const '(' (TERM*  (Const '>' TERM)*) ')'  Uniterm ::= Const '(' (TERM*  (Const '>' TERM)*) ')'  
+  Unicall ::= Const '(' TERM* ')'  
Equal ::= TERM '=' TERM  Equal ::= TERM '=' TERM  
Member ::= TERM '#' TERM  Member ::= TERM '#' TERM  
Subclass ::= TERM '##' TERM  Subclass ::= TERM '##' TERM  
Frame ::= TERM '[' (TERM '>' TERM)* ']'  Frame ::= TERM '[' (TERM '>' TERM)* ']'  
−  TERM ::= Const  Var   +  TERM ::= Const  Var  Uniterm  Unicall 
Const ::= '"' LITERAL '"^^' SYMSPACE  Const ::= '"' LITERAL '"^^' SYMSPACE  
Var ::= '?' VARNAME  Var ::= '?' VARNAME  
Line 287:  Line 288:  
−  The production rule for the nonterminal <tt>CONDITION</tt> represents ''RIF condition formulas'' (defined earlier). The connectives <tt>And</tt> and <tt>Or</tt> define conjunctions and disjunctions of conditions, respectively. <tt>Exists</tt> introduces existentially quantified variables. Here <tt>Var+</tt> stands for the list of variables that are free in <tt>CONDITION</tt>. RIFBLD conditions permit only existential variables, but [[FLD#secsyntacticframeworkRIFFLD Syntax]] allows arbitrary quantification, which can be used in some dialects. A <tt>CONDITION</tt> can also be  +  The production rule for the nonterminal <tt>CONDITION</tt> represents ''RIF condition formulas'' (defined earlier). The connectives <tt>And</tt> and <tt>Or</tt> define conjunctions and disjunctions of conditions, respectively. <tt>Exists</tt> introduces existentially quantified variables. Here <tt>Var+</tt> stands for the list of variables that are free in <tt>CONDITION</tt>. RIFBLD conditions permit only existential variables, but [[FLD#secsyntacticframeworkRIFFLD Syntax]] allows arbitrary quantification, which can be used in some dialects. A <tt>CONDITION</tt> can also be an <tt>ATOMIC</tt> term, i.e. a <tt>Uniterm</tt>, <tt>Unicall</tt>, <tt>Equal</tt>, <tt>Member</tt>, <tt>Subclass</tt>, or <tt>Frame</tt>. The production for the nonterminal <tt>TERM</tt> defines RIFBLD terms  constants, variables, <tt>Uniterm</tt>s, or <tt>Unicall</tt>s. 
−  The RIFBLD presentation syntax does not commit to any particular vocabulary for the names of variables or for the literals used in constant symbols. In the examples, variables are denoted by Unicode character sequences beginning with a ?sign. Constant symbols have the form: <tt>"LITERAL"^^SYMSPACE</tt>, where <tt>SYMSPACE</tt> is an IRI string that identifies the symbol space of the constant and <tt>LITERAL</tt> is a Unicode string from the lexical space of that symbol space. Equality, membership, and subclass terms are selfexplanatory. Uniterms (''Universal terms'') are terms that can be either positional or with named arguments. A frame term is a term composed of an object Id and a collection of attributevalue pairs.  +  The RIFBLD presentation syntax does not commit to any particular vocabulary for the names of variables or for the literals used in constant symbols. In the examples, variables are denoted by Unicode character sequences beginning with a ?sign. Constant symbols have the form: <tt>"LITERAL"^^SYMSPACE</tt>, where <tt>SYMSPACE</tt> is an IRI string that identifies the symbol space of the constant and <tt>LITERAL</tt> is a Unicode string from the lexical space of that symbol space. Equality, membership, and subclass terms are selfexplanatory. Uniterms (''Universal terms'') are predicate/function terms that can be either positional or with named arguments. A frame term is a term composed of an object Id and a collection of attributevalue pairs. 
+  Unicalls (''Universal calls'') are predicate/function terms with positional arguments that call any of the builtins of [[DTBRIFDTB]].  
Example 1 shows conditions that are composed of uniterms, frames, and  Example 1 shows conditions that are composed of uniterms, frames, and  
Line 345:  Line 347:  
−  <span id="secebnfrulelanguage" class="anchor"></span>  +  <span id="secebnfrulelanguage" class="anchor"></span> 
===== EBNF for RIFBLD Rule Language =====  ===== EBNF for RIFBLD Rule Language ===== 
Revision as of 14:01, 11 March 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 [[DTBRIF Data Types and BuiltIns] described 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) based on a set of foundational concepts that are supposed to be shared by all logicbased RIF dialects.
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 a lá Flogic [KLW95], internationalized resource identifiers (or IRIs, defined by RFC 3987 [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 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 RIFBLD. 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 RIFPRD), reactive rules, and normative rules.
RIFBLD is defined in two different ways  both normative. First, it is defined as a specialization of the RIF Framework for Logicbased Dialects (RIFFLD)  the RIF extensibility framework. It is a very short description, but it requires familiarity with RIFFLD. RIFFLD provides a general framework  both syntactic and semantic  for defining RIF dialects. All logicbased dialects are required to specialize this framework. Then RIFBLD is described independently of the RIF framework, for the benefit of those who desire a quicker path to RIFBLD and are not interested in the extensibility issues.
The current document is the third draft of the RIFBLD specification. A number of extensions are planned to support builtins, additional primitive XML data types, the notion of RIF compliance, and so on. Tool support for RIFBLD is forthcoming. RIF dialects that extend RIFBLD in accordance with the RIF Framework for Logic Dialects will be specified in other documents by this working group.
2 RIFBLD as a Specialization of RIFFLD
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 and proceed to Direct Specification of RIFBLD Syntax.
2.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 RIFFLD in that document lists the parameters of the syntactic framework, which we will now specialize for RIFBLD.
 Alphabet.
 The alphabet of RIFBLD is the alphabet of RIFFLD with the negation symbols neg and naf excluded
 Assignment of signatures to each constant symbol.
 The signature set of RIFBLD contains the following signatures:
 term{ },
 term_builtin{ },
 atomic{ },
 atomic_builtin{ },
 term_builtin<term and atomic_builtin<atomic.
 The signature term{ } represents the context in which individual objects (but not atomic formulas) can appear. The signature term_builtin{ } represents terms constructed with the use of builtin functions. The signature atomic_builtin{ } represents atomic formulas for builtin predicates (such as fn:substring). Since atomic_builtin<atomic, builtin atomic formulas are also atomic formulas, but normally most atomic formulas are userdefined and they will have the signature atomic rather than atomic_builtin.
 For every integer n ≥ 0, there are signatures
 f_{n}{(term ... term) ⇒ term}  for nary function symbols,
 p_{n}{(term ... term) ⇒ atomic}  for nary predicates,
 fip_{n}{(term ... term) ⇒ term_builtin}  for nary builtin functions, and
 bip_{n}{(term ... term) ⇒ atomic_builtin}  for nary builtin predicates.
 These represent function symbols of arity n, userdefined predicate symbols of arity n, and nary builtin predicates, respectively (each of the above cases has n termarguments inside the parentheses).
 For every set of symbols s1,...,sk ∈ SigNames, there are signatures f_{s1...sk}{(s1>term ... sk>term) ⇒ term} and p_{s1...sk}{(s1>term ... sk>term) ⇒ atomic}. These are signatures for terms with named arguments and predicates with arguments named s1, ..., sk, respectively. Unlike in RIFFLD, the argument names s1, ..., sk must be pairwise distinct.
 A symbol in Const can have exactly one signature, term, f_{n}, p_{n}, or bip_{n}, where n ≥ 0, or f_{s1...sk}{(s1>term ... sk>term) ⇒ term}, p_{s1...sk}{(s1>term ... sk>term) ⇒ atomic}, for some s1,...,sk ∈ SigNames. It cannot have the signature atomic or atomic_builtin, 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 predicate of one particular arity or with certain argument names, a builtin of one particular arity, or a function symbol of one particular arity  it is not possible for the same symbol to play more than one role.
 The constant symbols that correspond to XML Schema data types all have the signature term in RIFBLD. The symbols of type rif:iri and rif:local can have the following signatures in RIFBLD: term, f_{n}, p_{n}, or bip_{n}, for n = 0,1,....; or f_{s1...sk}, p_{s1...sk}, for some argument names s1,...,sk ∈ SigNames.
 All variables are associated with signature term{ }, so they can range only over individuals.
 The signature for equality is ={(term term) ⇒ atomic}. This means that equality can compare only those terms whose signature is term; 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 term.
 The frame signature, >, is >{(term term term) ⇒ 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 #{(term term) ⇒ 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 ##{(term term) ⇒ atomic}. As with frames and membership terms, this precludes the possibility that a subclass term might occur inside some other term.
 RIFBLD uses no extra syntax for declaring signatures. Instead, signatures are inferred. Since RIFBLD requires that each symbol is associated with a unique signature, the signature can be determined from the context in which the symbol is used. If a symbol is used in more than one context, the parser should treat it as a syntax error. If no errors are found, all terms and atomic formulas are guaranteed to be wellformed. As a consequence, signatures are not part of the RIFBLD language and term, atomic, and atomic_builtin are not reserved keywords in RIFBLD.
 The signature set of RIFBLD contains the following signatures:
 Supported types of terms.
 RIFBLD supports all the term types defined by the syntactic framework (see Wellformed Terms and Formulas):
 constants
 variables
 positional
 with named arguments
 equality
 frame
 membership
 subclass
 Compared to RIFFLD, terms (both positional and with named arguments) have significant restrictions. This is so as to keep BLD a relatively compact nature.
 The signature for the variable symbols does not permit them to occur in the context of predicates, functions, or formulas. In particular, unlike in RIFFLD, a variable is not an atomic formula in RIFBLD.
 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 term{ } and all other terms, except for the constants from Const, can have either the signature term{ } or atomic{ }. Therefore, if t is a (nonConst) term then t(...) is not a wellformed term.
 RIFBLD supports all the term types defined by the syntactic framework (see Wellformed Terms and Formulas):
 Supported symbol spaces.
 RIFBLD supports all the symbol spaces defined in Section Symbol Spaces of the syntactic framework:
 xsd:string
 xsd:decimal
 xsd:time
 xsd:date
 xsd:dateTime
 rdf:XMLLiteral
 rif:text
 rif:iri
 rif:local
 RIFBLD supports all the symbol spaces defined in Section Symbol Spaces of the syntactic framework:
 Supported formulas.
 RIFBLD supports the following types of formulas (see Wellformed Terms and Formulas for the definitions):
 RIFBLD condition
 A RIFBLD condition is a conjunctive and disjunctive combination of atomic formulas with optional existential quantification of variables.
 RIFBLD rule
 A RIFBLD rule is a RIFFLD rule with the following restrictions:
 The head (or conclusion) of the rule is an atomic formula, which is not a builtin predicate (i.e., its signature is atomic, but not atomic_builtin).
 The body (or premise) of the rule is a RIFBLD condition.
 The free (nonquantified) variables in the rule must be quantified with Forall outside of the rule (i.e., Forall ?vars (head : body)).
 A RIFBLD rule is a RIFFLD rule with the following restrictions:
 RIFBLD condition
 RIFBLD supports the following types of formulas (see Wellformed Terms and Formulas for the definitions):
Recall that negation (classical or default) is not supported by RIFBLD in either the rule head or the body.
The list of supported symbol spaces will move to another document, Data Types and BuiltIns. Any existing discrepancies will be fixed at that time. 
2.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 without reference to 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 RIFFLD in that document lists the parameters of the semantic framework, which we need to specialize for RIFBLD.
Recall that the semantics of a dialect is derived from these notions by specializing the following parameters.
 The effect of the syntax.
 RIFBLD does not support negation. This is the only obvious simplification with respect to RIFFLD as far as the semantics is concerned.
 Truth values.
 The set TV of truth values in RIFBLD consists of just two values, t and f such that f <_{t} t. Clearly, <_{t} is a total order here.
 Data types.
 RIFBLD supports all the data types listed in Section Primitive Data Types of RIFFLD:
 xsd:long
 xsd:integer
 xsd:decimal
 xsd:string
 xsd:time
 xsd:dateTime
 rdf:XMLLiteral
 rif:text
 RIFBLD supports all the data types listed in Section Primitive Data Types of RIFFLD:
 Logical entailment.
 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:
 as a set of all models; or
 as the unique minimal model.
 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 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].
The list of supported data types will move to another document, Data Types and BuiltIns. Any existing discrepancies will be fixed at that time. 
3 Direct Specification of RIFBLD Syntax
This normative section specifies the syntax of RIFBLD directly, without referring to 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 intended 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.
3.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 and Or, quantifiers Exists and Forall, the symbols =, #, ##, >, :, and auxiliary symbols, such as "(" and ")". The set of connective symbols, quantifiers, =, etc., is disjoint from Const and Var. 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 "?". The syntax for constant symbols is given in Section Symbol Spaces of RIFFLD. ☐
The language of RIFBLD is the set of formulas constructed using the above alphabet according to the rules spelled out below.
3.2 Terms
RIFBLD supports several kinds of terms: constants and variables, positional terms, terms with named arguments, equality, membership, and subclass terms, and frames. The word "term" will be used to refer to any kind of terms.
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 term 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. ☐
Membership, subclass, and frame terms are used to describe objects and class hierarchies. These terms can be readily mixed both with positional terms and terms with named arguments: p(?X q#r[v(1,2)>s] t(d>e f>g)).
3.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; and
 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), which are allowed for that symbol.
The arity of a symbol (or whether it is a predicate, a function, or an individual) is not specified explicitly in RIFBLD. Instead, it is inferred as follows. Each constant symbol in a RIFBLD formula (or a set of formulas) may occur in at most one context: as an individual, a function symbol of a particular arity, or a predicate symbol of a particular arity. The arity of the symbol and its type is then determined by its context. If a symbol from Const occurs in more than one context in a set of formulas, the set considered to be not wellformed in RIFBLD.
3.4 Formulas
Any term (positional or with named arguments) of the form p(...), where p is a predicate symbol, is also an atomic formula. Equality, membership, subclass, and frame terms are also atomic formulas. 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}). 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}). When n=0, we get Or() as a special case; it is treated as 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 a formula.
Formulas constructed using the above definitions are called RIFBLD conditions. The following formulas lead to the notion of a RIFBLD rule.
 Rule implication: If φ is an wellformed atomic formula and ψ is a RIFBLD condition then φ : ψ is a wellformed formula, provided that φ does not have the signature atomic_builtin (i.e., is not a builtin predicate).
 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 an explicitly quantified rule.
Quantified rules are also referred to as RIFBLD rules.
A set of RIFBLD rules and atomic formulas (often referred to as facts) is called a ruleset. ☐
It can be seen from the definitions that RIFBLD has a wide variety of syntactic forms for terms, formulas, and rules. This provides the infrastructure for exchanging rule languages that support rich collections of syntactic forms. Systems that do not support some of that syntax directly can still support it through a syntactic transformation. For instance, disjunctions in the rule body can be eliminated through a standard transformation, such as p : Or(q r) to {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).
3.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 on intentionally, since RIF's presentation syntax is intended as a tool for specifying the semantics and for illustration of the main RIF concepts through examples. It is not intended as a concrete syntax for a rule language. RIF defines a concrete syntax only for exchanging rules, and that syntax is XMLbased, obtained as a refinement and serialization of the EBNF syntax.
 For all the above reasons, the EBNF syntax is not normative.
3.5.1 EBNF for RIFBLD Condition Language
The Condition Language represents formulas that can be used in the body of the RIFBLD 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 RIFBLD condition language is as follows.
CONDITION ::= 'And' '(' CONDITION* ')'  'Or' '(' CONDITION* ')'  'Exists' Var+ '(' CONDITION ')'  ATOMIC ATOMIC ::= Uniterm  Unicall  Equal  Member  Subclass  Frame Uniterm ::= Const '(' (TERM*  (Const '>' TERM)*) ')' Unicall ::= Const '(' TERM* ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '>' TERM)* ']' TERM ::= Const  Var  Uniterm  Unicall Const ::= '"' LITERAL '"^^' SYMSPACE Var ::= '?' VARNAME
The production rule for the nonterminal CONDITION represents RIF condition formulas (defined earlier). The connectives And and Or define conjunctions and disjunctions of conditions, respectively. Exists introduces existentially quantified variables. Here Var+ stands for the list of variables that are free in CONDITION. RIFBLD conditions permit only existential variables, but RIFFLD Syntax allows arbitrary quantification, which can be used in some dialects. A CONDITION can also be an ATOMIC term, i.e. a Uniterm, Unicall, Equal, Member, Subclass, or Frame. The production for the nonterminal TERM defines RIFBLD terms  constants, variables, Uniterms, or Unicalls.
The RIFBLD presentation syntax does not commit to any particular vocabulary for the names of variables or for the literals used in constant symbols. In the examples, variables are denoted by Unicode character sequences beginning with a ?sign. Constant symbols have the form: "LITERAL"^^SYMSPACE, where SYMSPACE is an IRI string that identifies the symbol space of the constant and LITERAL is a Unicode string from the lexical space of that symbol space. Equality, membership, and subclass terms are selfexplanatory. Uniterms (Universal terms) are predicate/function terms that can be either positional or with named arguments. A frame term is a term composed of an object Id and a collection of attributevalue pairs. Unicalls (Universal calls) are predicate/function terms with positional arguments that call any of the builtins of RIFDTB.
Example 1 shows conditions that are composed of uniterms, frames, and existentials. The examples of the frames show that variables can occur in the syntactic positions of object Ids, object properties, or property values. For brevity, this and other examples uses the compact URI notation [CURIE], prefix:suffix, which is a macro that expands into a concatenation of the prefix definition and suffix.
Example 1 (RIFBLD conditions) We use the prefix bks to abbreviate http://example.com/books#, the prefix auth for http://example.com/authors#, and the prefix cpt for 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"^^rif:iri>"auth:rifwg"^^rif:iri "cpt:title"^^rif:iri>"bks:LeRif"^^rif:iri) Exists ?X ("cpt:book"^^rif:iri("cpt:author"^^rif:iri>?X "cpt:title"^^rif:iri>"bks:LeRif"^^rif:iri)) Frames: "bks:wd1"^^rif:iri["cpt:author"^^rif:iri>"auth:rifwg"^^rif:iri "cpt:title"^^rif:iri>"bks:LeRif"^^rif:iri ] Exists ?X ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri>?X "cpt:title"^^rif:iri>"bks:LeRif"^^rif:iri ]) Exists ?X ("bks:wd2"^^rif:iri # "cpt:book"^^rif:iri["cpt:author"^^rif:iri>?X "cpt:title"^^rif:iri>"bks:LeRif"^^rif:iri]) Exists ?I ?X (?I["cpt:author"^^rif:iri>?X "cpt:title"^^rif:iri>"bks:LeRif"^^rif:iri]) Exists ?I ?X (?I # "cpt:book"^^rif:iri["cpt:author"^^rif:iri>?X "cpt:title"^^rif:iri>"bks:LeRif"^^rif:iri]) Exists ?S ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri>"auth:rifwg"^^rif:iri ?S>"bks:LeRif"^^rif:iri]) Exists ?X ?S ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri>?X ?S>"bks:LeRif"^^rif:iri]) Exists ?I ?X ?S (?I # "cpt:book"^^rif:iri[author>?X ?S>"bks:LeRif"^^rif:iri])
3.5.2 EBNF for RIFBLD Rule Language
The presentation syntax for Horn rules extends the syntax in Section EBNF for RIFBLD Condition Language with the following productions.
Ruleset ::= RULE* RULE ::= 'Forall' Var+ '(' RULE ')'  Implies  COMPOUND Implies ::= COMPOUND ':' CONDITION
A Ruleset is a set of RIF rules. Rules are generated by the Implies production, with optional Forallquantification. Var, COMPOUND, and CONDITION were defined as part of the syntax for positive conditions in Section EBNF for RIFBLD Condition Language. Note that COMPOUND terms are treated as rules with an empty condition part  they are usually called facts. Note that, by a definition in Section Formulas, atomic formulas that correspond to builtin predicates (i.e., formulas with signature atomic_builtin) are not allowed in the conclusion part of a rule. This restriction is not reflected in the EBNF syntax.
The document RIF Use Cases and Requirements includes a use case "Negotiating eBusiness Contracts Across Rule Platforms", which discusses a business rule slightly modified here:
If an item is perishable and it is delivered to John more than 10 days after the scheduled delivery date then the item will be rejected by him.
In the Presentation EBNF Syntax used throughout this document, this rule can be written in one of these two equivalent ways:
Example 2 (RIFBLD rules) Here we use the prefix ppl as an abbreviation for http://example.com/people# and the prefix cpt for http://example.com/concepts# The prefix op is used for a yettobedetermined IRI, which will be used 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) "fn:subtractdateTimesyieldingdayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration) "fn:getdaysfromdayTimeDuration"^^rif:iri(?diffduration ?diffdays) "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) "fn:subtractdateTimesyieldingdayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration) "fn:getdaysfromdayTimeDuration"^^rif:iri(?diffduration ?diffdays) "op:numericgreaterthan"^^rif:iri(?diffdays "10"^^xsd:integer)) ) )
4 Direct Specification of RIFBLD Semantics
This normative section specifies the semantics of RIFBLD directly, without referring to RIFFLD.
4.1 Truth Values
The set TV of truth values in RIFBLD consists of just two values, t and f. This set has a total order, called truth order, such that f <_{t} t.
4.2 Semantic Structures
Definition (Semantic structure). A semantic structure, I, is a tuple of the form <TV, DTS, D, I_{C}, I_{V}, I_{F}, I_{frame}, I_{SF}, I_{sub}, I_{isa}, I_{=}, I_{Truth}>. Here D is a nonempty set of elements called the domain of I, and there is a proper subset, D_{ind} ⊂D, which is used to interpret individuals. We use Const to refer to the set of all constant symbols and Var to refer to the set of all variable symbols. TV denotes the set of truth values that the semantic structure uses and DTS is the set of primitive data types used in I (please refer to Section Primitive Data Types of RIFFLD for the semantics of data types).
The other components of I are total mappings defined as follows:
 I_{C} maps Const to elements of D.
 This mapping interprets constant symbols.
If a constant, c ∈ Const, occurs in the position of an individual then it is required that I_{C}(c) ∈ D_{ind}.
 I_{V} maps Var to elements of D_{ind}.
 This mapping interprets variable symbols.
 I_{F} maps D to functions D* → D (here D* is a set of all sequences of any finite length over the domain D)
 This mapping interprets positional terms.
 I_{SF} interprets terms with named arguments. It is a total mapping from Const to the set of total functions of the form SetOfFiniteSets(ArgNames × D) → D. This is analogous to the interpretation of positional terms with two differences:
 Each pair <s,v> ∈ ArgNames × D represents a argument/value pair instead of just a value in the case of a positional term.
 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} is a total mapping from D to total functions of the form SetOfFiniteBags(D × D) → D.
 This mapping interprets frame terms. An argument, d ∈ D, to I_{frame} represent an object and the finite bag {<a1,v1>, ..., <ak,vk>} represents a bag of 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. For instance, o[a>b a>b].
 I_{sub} gives meaning to the subclass relationship. It is a total function D × D → D.
 The operator ## is required to be transitive, i.e., c1 ## c2 and c2 ## c3 must imply c1 ## c3. This is ensured by a restriction in Section Interpretation of Formulas.
 I_{isa} gives meaning to class membership. It is a total function D × D → D.
 The relationships # and ## are required to have the usual property that all members of a subclass are also members of the superclass, i.e., o # cl and cl ## scl must imply o # scl. This is ensured by a restriction in Section Interpretation of Formulas.
 I_{=} gives meaning to the equality. It is a total function D × D → D.
 I_{Truth} is a total mapping D → TV.
 It is used to define truth valuation of formulas.
We also define the following mapping I :
 I(k) = I_{C}(k), if k is a symbol in Const
 I(?v) = I_{V}(?v), if ?v is a variable in Var
 I(f(t_{1} ... t_{n})) = I_{F}(I(f))(I(t_{1}),...,I(t_{n}))
 I(f(s_{1}>v_{1} ... s_{n}>v_{n})) = I_{SF}(I(f))({<s_{1},I(v_{1})>,...,<s_{n},I(v_{n})>})
 Here we use {...} to denote a set of argument/value pairs.
 I(o[a_{1}>v_{1} ... a_{k}>v_{k}]) = I_{frame}(I(o))({<I(a_{1}),I(v_{1})>, ..., <I(a_{n}),I(v_{n})>})
 Here {...} denotes a bag of attribute/value pairs.
 I(c1##c2) = I_{sub}(I(c1), I(c2))
 I(o#c) = I_{isa}(I(o), I(c))
 I(x=y) = I_{=}(I(x), I(y))
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; 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. ☐
4.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.
 Subclass: TVal_{I}(sc ## cl) = I_{Truth}(I(sc ## cl)).
 To ensure that the operator ## is transitive, i.e., c1 ## c2 and c2 ## c3 imply c1 ## c3, the following is required: For all c1, c2, c3 ∈ D, min_{t}(TVal_{I}(c1 ## c2), TVal_{I}(c2 ## c3)) ≤_{t} TVal_{I}(c1 ## c3).
 Membership: TVal_{I}(o # cl) = I_{Truth}(I(o # cl)).
 To ensure that all members of a subclass are also members of the superclass, i.e., o # cl and cl ## scl implies o # scl, the following is required: For all o, cl, scl ∈ D, min_{t}(TVal_{I}(o # cl), TVal_{I}(cl ## scl)) ≤_{t} TVal_{I}(o # scl).
 Frame: TVal_{I}(o[a_{1}>v_{1} ... a_{k}>v_{k}]) = I_{Truth}(I(o[a_{1}>v_{1} ... a_{k}>v_{k}])).
 Since the different attribute/value pairs are supposed to be understood as conjunctions, the following is required:
 TVal_{I}(o[a_{1}>v_{1} ... a_{k}>v_{k}]) = min_{t}(TVal_{I}(o[a_{1}>v_{1}]), ..., TVal_{I}(o[a_{k}>v_{k}]))
 Since the different attribute/value pairs are supposed to be understood as conjunctions, the following is required:
 Conjunction: TVal_{I}(And(c_{1} ... c_{n})) = min_{t}(TVal_{I}(c_{1}), ..., TVal_{I}(c_{n})).
 Disjunction: TVal_{I}(Or(c_{1} ... c_{n})) = max_{t}(TVal_{I}(c_{1}), ..., TVal_{I}(c_{n})).
 Quantification: TVal_{I}(Exists ?v_{1} ... ?v_{n} (φ)) = max_{t}(TVal_{I*}(φ)) and TVal_{I}(Forall ?v_{1} ... ?v_{n} (φ)) = min_{t}(TVal_{I*}(φ)).
Here max_{t} (respectively, min_{t}) is taken over all interpretations I* of the form <TV, DTS, D, I_{C}, I*_{V}, I_{F}, I_{frame}, I_{SF}, I_{sub}, I_{isa}, I_{Truth}>, which are exactly like I, except that the mapping I*_{V}, is used instead of I_{V}. I*_{V} is defined to coincide with I_{V} on all variables except, possibly, on ?v_{1},...,?v_{n}.
 Rules: TVal_{I}(conclusion : condition) = t, if TVal_{I}(conclusion) ≥_{t} TVal_{I}(condition); TVal_{I}(conclusion : condition) = f otherwise.
A model of a set Ψ of formulas is a semantic structure I such that TVal_{I}(φ) = t for every φ∈Ψ. In this case, we write I = Ψ. ☐
4.4 Logical Entailment
We now define what it means for a set of RIFBLD rules to entail a RIFBLD condition.
A RIF 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 R be a set of RIFBLD rules and φ an existentially closed RIFBLD condition formula. We say that R entails φ, written as R = φ, if and only if for every semantic structure I of R and every ψ ∈ R, it is the case that TVal_{I}(ψ) ≤ TVal_{I}(φ).
Equivalently, we can say that R = φ holds iff whenever I = R it follows that also I = φ. ☐
5 XML Serialization Syntax for RIFBLD
The XML serialization for RIFBLD presentation syntax given in this section is alternating or fully striped (e.g., [ANF01]). Positional information is optionally exploited only for the arg role elements. For example, role elements (declare and formula) are explicit within the Exists element. Following the examples of Java and RDF, we use capitalized names for class elements and names that start with lowercase for role elements.
The alluppercase classes in the presentation syntax, such as CONDITION, become XML entities. They act like macros and are not visible in instance markup. The other classes as well as nonterminals and symbols (such as Exists or =) become XML elements with optional attributes, as shown below.
5.1 XML for RIFBLD Condition Language
We now serialize the syntax of Section EBNF for RIFBLD Condition Language in XML.
Classes, roles and their intended meaning  And (conjunction)  Or (disjunction)  Exists (quantified formula for 'Exists', containing declare and formula roles)  declare (declare role, containing a Var)  formula (formula role, containing a CONDITION formula)  Uniterm (term or atomic formula, positional or with named arguments)  Member (member formula)  Subclass (subclass formula)  Frame (Frame formula)  object (Member/Frame role containing a TERM or an object description)  op (Uniterm role for predicates/functions as operations)  arg (argument role)  upper (Member/Subclass upper class role)  lower (Member/Subclass lower instance/class role)  slot (Uniterm/Frame slot role, prefix version of slot infix ' > ')  Equal (prefix version of term equation '=')  side (Equal lefthand side and righthand side role)  Const (slot, individual, function, or predicate symbol, with optional 'type' attribute)  Var (logic variable)
For the XML Schema Definition (XSD) of the RIFBLD condition language see Appendix [[#secbldxsdXML 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>.
The following example illustrates XML serialization of RIF conditions.
Example 3 (A RIF condition and its XML serialization): We use the prefix bks as an abbreviation for http://example.com/books#, cpt for http://example.com/concepts#, and curr for http://example.com/currencies# a. 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 ) b. XML serialization <And> <formula> <Exists> <declare><Var>Buyer</Var></declare> <formula> <Uniterm> <op><Const type="rif:iri">cpt:purchase</Const></op> <arg><Var>Buyer</Var></arg> <arg><Var>Seller</Var></arg> <arg> <Uniterm> <op><Const type="rif:iri">cpt:book</Const></op> <arg><Var>Author</Var></arg> <arg><Const type="rif:iri">bks:LeRif</Const></arg> </Uniterm> </arg> <arg> <Uniterm> <op><Const type="rif:iri">curr:USD</Const></op> <arg><Const type="xsd:integer">49</Const></arg> </Uniterm> </arg> </Uniterm> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And>
The following example illustrates XML serialization of RIF conditions that involve terms with named arguments.
Example 4 (A RIF condition and its XML serialization): We use the prefix bks to abbreviate http://example.com/books#, the prefix auth for http://example.com/authors#, the prefix cpt for http://example.com/concepts#, and curr for http://example.com/currencies#. a. RIF condition: And (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"^^rif:iri> ?Author "cpt:title"^^rif:iri> "bks:LeRif"^^rif:iri ) "cpt:price"^^rif:iri> "49"^^xsd:integer "cpt:currency"^^rif:iri> "curr:USD"^^rif:iri ] ) ?Seller=?Author ) b. XML serialization: <And> <formula> <Exists> <declare><Var>Buyer</Var></declare> <declare><Var>P</Var></declare> <formula> <Frame> <object> <Member> <lower><Var>P</Var></lower> <upper><Const type="rif:iri">cpt:purchase</Const></upper> </Member> </object> <slot><Const type="rif:iri">cpt:buyer</Const><Var>Buyer</Var></slot> <slot><Const type="rif:iri">cpt:seller</Const><Var>Seller</Var></slot> <slot> <Const type="rif:iri">cpt:item</Const> <Uniterm> <op><Const type="rif:iri">cpt:book</Const></op> <slot><Const type="rif:iri">cpt:author</Const><Var>Author</Var></slot> <slot><Const type="rif:iri">cpt:title</Const><Const type="rif:iri">bks:LeRif</Const></slot> </Uniterm> </slot> <slot><Const type="rif:iri">cpt:price</Const><Const type="xsd:integer">49</Const></slot> <slot><Const type="rif:iri">cpt:currency</Const><Const type="rif:iri">curr:USD</Const></slot> </Frame> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And>
5.2 XML for RIFBLD Rule Language
The following extends the XML syntax in Section XML for RIFBLD Condition Language, by serializing the syntax of Section EBNF for RIFBLD Rule Language in XML. The Forall element contains the role elements declare and formula, which were earlier used within the Exists element in Section XML for RIFBLD Condition Language. The Implies element contains the role elements if and then to designate these two parts of a rule.
Classes, roles and their intended meaning  Ruleset (rule collection, containing rule roles)  Forall (quantified formula for 'Forall', containing declare and formula roles)  Implies (implication, containing if and then roles)  if (antecedent role, containing CONDITION)  then (consequent role, containing a Uniterm, Equal, or Frame)
For the XML Schema Definition (XSD) of the RIFBLD Horn rule language see Appendix XML Schema for BLD.
For instance, the rule in Example 5a can be serialized in XML as shown below as the first element of a ruleset whose second element is a business rule for Fred.
Example 5 (A RIF ruleset in XML syntax) <Ruleset> <rule> <Forall> <declare><Var>item</Var></declare> <declare><Var>deliverydate</Var></declare> <declare><Var>scheduledate</Var></declare> <declare><Var>diffduration</Var></declare> <declare><Var>diffdays</Var></declare> <formula> <Implies> <if> <And> <formula> <Uniterm> <op><Const type="rif:iri">cpt:perishable</Const></op> <arg><Var>item</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <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> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:iri">cpt:scheduled</Const></op> <arg><Var>item</Var></arg> <arg><Var>scheduledate</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:iri">fn:subtractdateTimesyieldingdayTimeDuration</Const></op> <arg><Var>deliverydate</Var></arg> <arg><Var>scheduledate</Var></arg> <arg><Var>diffduration</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:iri">fn:getdaysfromdayTimeDuration</Const></op> <arg><Var>diffduration</Var></arg> <arg><Var>diffdays</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:iri">op:numericgreaterthan</Const></op> <arg><Var>diffdays</Var></arg> <arg><Const type="xsd:long">10</Const></arg> </Uniterm> </formula> </And> </if> <then> <Uniterm> <op><Const type="xsd:long">reject</Const></op> <arg><Const type="rif:iri">ppl:John</Const></arg> <arg><Var>item</Var></arg> </Uniterm> </then> </Implies> </formula> </Forall> </rule> <rule> <Forall> <declare><Var>item</Var></declare> <formula> <Implies> <if> <Uniterm> <op><Const type="rif:iri">cpt:unsolicited</Const></op> <arg><Var>item</Var></arg> </Uniterm> </if> <then> <Uniterm> <op><Const type="rif:iri">cpt:reject</Const></op> <arg><Const type="rif:iri">ppl:Fred</Const></arg> <arg><Var>item</Var></arg> </Uniterm> </then> </Implies> </formula> </Forall> </rule> </Ruleset>
5.3 Translation Between the RIFBLD Presentation and XML Syntaxes
We now show how to translate between the presentation and XML syntaxes of RIFBLD.
5.3.1 Translation of RIFBLD Condition Language
The translation between the presentation syntax and the XML syntax of the RIFBLD Condition Language is given by a table as follows.
Presentation Syntax  XML Syntax 

And ( conjunct_{1} . . . conjunct_{n} ) 
<And> <formula>conjunct_{1}</formula> . . . <formula>conjunct_{n}</formula> </And> 
Or ( disjunct_{1} . . . disjunct_{n} ) 
<Or> <formula>disjunct_{1}</formula> . . . <formula>disjunct_{n}</formula> </Or> 
Exists variable_{1} . . . variable_{n} ( body ) 
<Exists> <declare>variable_{1}</declare> . . . <declare>variable_{n}</declare> <formula>body</formula> </Exists> 
predfunc ( argument_{1} . . . argument_{n} ) 
<Uniterm> <op>predfunc</op> <arg>argument_{1}</arg> . . . <arg> argument_{n}</arg> </Uniterm> 
predfunc ( key_{1} > filler_{1} . . . key_{n} > filler_{n} ) 
<Uniterm> <op>predfunc</op> <slot>key_{1} filler_{1}</slot> . . . <slot>key_{n} filler_{n}</slot> </Uniterm> 
inst [ key_{1} > filler_{1} . . . key_{n} > filler_{n} ] 
<Frame> <object>inst</object> <slot>key_{1} filler_{1}</slot> . . . <slot>key_{n} filler_{n}</slot> </Frame> 
inst # class [ key_{1} > filler_{1} . . . key_{n} > filler_{n} ] 
<Frame> <object> <Member> <lower>inst</lower> <upper>class</upper> </Member> </object> <slot>key_{1} filler_{1}</slot> . . . <slot>key_{n} filler_{n}</slot> </Frame> 
sub ## super [ key_{1} > filler_{1} . . . key_{n} > filler_{n} ] 
<Frame> <object> <Subclass> <lower>sub</lower> <upper>super</upper> </Subclass> </object> <slot>key_{1} filler_{1}</slot> . . . <slot>key_{n} filler_{n}</slot> </Frame> 
inst # class 
<Member> <lower>inst</lower> <upper>class</upper> </Member> 
sub ## super 
<Subclass> <lower>sub</lower> <upper>super</upper> </Subclass> 
left = right 
<Equal> <side>left</side> <side>right</side> </Equal> 
name^^space 
<Const type="space">name</Const> 
?name 
<Var>name</Var> 
5.3.2 Translation of RIFBLD Rule Language
The translation between the presentation syntax and the XML syntax of the RIFBLD Rule Language is given by a table that extends the translation table of Section Translation of RIFBLD Condition Language as follows.
Presentation Syntax  XML Syntax 

Ruleset ( clause_{1} . . . clause_{n} ) 
<Ruleset> <rule>clause_{1}</rule> . . . <rule>clause_{n}</rule> </Ruleset> 
Forall variable_{1} . . . variable_{n} ( rule ) 
<Forall> <declare>variable_{1}</declare> . . . <declare>variable_{n}</declare> <formula>rule</formula> </Forall> 
conclusion : condition 
<Implies> <if>condition</if> <then>conclusion</then> </Implies> 
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.
 [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 http://www.jdrew.org/rif/wd2/ 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.7 20080212 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: CONDITION ::= 'And' '(' CONDITION* ')'  'Or' '(' CONDITION* ')'  'Exists' Var+ '(' CONDITION ')'  COMPOUND COMPOUND ::= Uniterm  Equal  Member  Subclass  Frame Uniterm ::= Const '(' (TERM*  (Const '>' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '>' TERM)* ']' TERM ::= Const  Var  COMPOUND Const ::= '"' LITERAL '"^^' SYMSPACE Var ::= '?' VARNAME </xs:documentation> </xs:annotation> <xs:group name="CONDITION"> <! CONDITION ::= 'And' '(' CONDITION* ')'  'Or' '(' CONDITION* ')'  'Exists' Var+ '(' CONDITION ')'  COMPOUND > <xs:choice> <xs:element ref="And"/> <xs:element ref="Or"/> <xs:element ref="Exists"/> <xs:group ref="COMPOUND"/> </xs:choice> </xs:group> <xs:element name="And"> <xs:complexType> <xs:sequence> <xs:element ref="formula" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Or"> <xs:complexType> <xs:sequence> <xs:element ref="formula" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Exists"> <xs:complexType> <xs:sequence> <xs:element ref="declare" minOccurs="1" maxOccurs="unbounded"/> <xs:element ref="formula"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="formula"> <xs:complexType> <xs:sequence> <xs:group ref="CONDITION"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="declare"> <xs:complexType> <xs:sequence> <xs:element ref="Var"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="COMPOUND"> <! COMPOUND ::= Uniterm  Equal  Member  Subclass  Frame > <xs:choice> <xs:element ref="Uniterm"/> <xs:element ref="Equal"/> <xs:element ref="Member"/> <xs:element ref="Subclass"/> <xs:element ref="Frame"/> </xs:choice> </xs:group> <xs:element name="Uniterm"> <! Uniterm ::= Const '(' (TERM*  (Const '>' TERM)*) ')' > <xs:complexType> <xs:sequence> <xs:element ref="op"/> <xs:choice> <xs:element ref="arg" minOccurs="0" maxOccurs="unbounded"/> <xs:element ref="slot" minOccurs="0" maxOccurs="unbounded"/> </xs:choice> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="op"> <xs:complexType> <xs:sequence> <xs:element ref="Const"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="arg"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="slot"> <xs:complexType> <xs:sequence> <xs:element ref="Const"/> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Equal"> <! Equal ::= TERM '=' TERM > <xs:complexType> <xs:sequence> <xs:element ref="side"/> <xs:element ref="side"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="side"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Member"> <! Member ::= TERM '#' TERM > <xs:complexType> <xs:sequence> <xs:element ref="lower"/> <xs:element ref="upper"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Subclass"> <! Subclass ::= TERM '##' TERM > <xs:complexType> <xs:sequence> <xs:element ref="lower"/> <xs:element ref="upper"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="lower"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="upper"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Frame"> <! Frame ::= TERM '[' (TERM '>' TERM)* ']' > <xs:complexType> <xs:sequence> <xs:element ref="object"/> <xs:element name="slot" minOccurs="0" maxOccurs="unbounded"> <! note difference from slot in Uniterm > <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="object"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="TERM"> <! TERM ::= Const  Var  COMPOUND > <xs:choice> <xs:element ref="Const"/> <xs:element ref="Var"/> <xs:group ref="COMPOUND"/> </xs:choice> </xs:group> <xs:element name="Const"> <! Const ::= '"' LITERAL '"^^' SYMSPACE > <xs:complexType mixed="true"> <xs:sequence/> <xs:attribute name="type" type="xs:string" use="required"/> </xs:complexType> </xs:element> <xs:element name="Var" type="xs:string"> <! Var ::= '?' VARNAME > </xs:element> </xs:schema>
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.7 20080212 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 ::= Ruleset* Ruleset ::= RULE* RULE ::= 'Forall' Var+ '(' RULE ')'  Implies  COMPOUND Implies ::= COMPOUND ':' CONDITION Note that this is an extension of the syntax for the RIFBLD Condition Language (BLDCond.xsd). </xs:documentation> </xs:annotation> <! The Rule Language includes the Condition Language> <xs:include schemaLocation="BLDCond.xsd"/> <xs:element name="Document"> <! Document ::= Ruleset* > <xs:complexType> <xs:sequence> <xs:element ref="Ruleset" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Ruleset"> <! Ruleset ::= RULE* > <xs:complexType> <xs:sequence> <xs:element ref="rule" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="rule"> <xs:complexType> <xs:sequence> <xs:group ref="RULE"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="RULE"> <! RULE ::= 'Forall' Var+ '(' RULE ')'  Implies  COMPOUND > <xs:choice> <xs:element ref="Forall"/> <xs:element ref="Implies"/> <xs:group ref="COMPOUND"/> </xs:choice> </xs:group> <xs:element name="Forall"> <xs:complexType> <xs:sequence> <xs:element ref="declare" minOccurs="1" maxOccurs="unbounded"/> <! note different from formula in And, Or and Exists > <xs:element name="formula"> <xs:complexType> <xs:group ref="RULE"/> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Implies"> <! Implies ::= COMPOUND ':' CONDITION > <xs:complexType> <xs:sequence> <xs:element ref="if"/> <xs:element ref="then"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="if"> <xs:complexType> <xs:sequence> <xs:group ref="CONDITION"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="then"> <xs:complexType> <xs:sequence> <xs:group ref="COMPOUND"/> </xs:sequence> </xs:complexType> </xs:element> </xs:schema>