Copyright © 2007 W3C^{®} (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark and document use rules apply.
This document, developed by the Rule Interchange Format (RIF) Working Group, specifies a basic format that allows logic rules to be exchanged between rule-based systems.
As part of its Phase 1 deliverable, the RIF Working Group defines a condition language, which is envisioned to be a shared part of all RIF dialects. The RIF Condition Language is intended to be used in the bodies of the rules in RIF Basic Logic Dialect (RIF-BLD). The condition language is then extended to Horn rules and this document specifies a presentation syntax and a corresponding concrete XML syntax for RIF-BLD. A model-theoretic semantics for the language is also defined.
This section describes the status of this document at the time of its publication. Other documents may supersede this document. A list of current W3C publications and the latest revision of this technical report can be found in the W3C technical reports index at http://www.w3.org/TR/.
This document is being published along with a draft of RIF RDF and OWL Compatibility. The two documents have been developed together and many readers will want to read them together. The Working Group has also published a Working Draft, RIF Use Cases and Requirements.
This First Public Working Draft represents a major evolution of the RIF Core Design (30 March 2007) Working Draft. The name change to "Basic Logic Dialect" represents an understanding in the group that this dialect may not be common to all rule languages. The major changes to the dialect since the RIF Core working draft include the removal of sorts from the semantics, the addition of frames, the addition of "slotted" or keyword arguments, and the removal of the OWL and RDF compatibility sections to a separate document published alongside this one. Major issues remaining with this draft are documented on the Working Group's issues page, and include whether to include membership and subclass in the frame syntax, whether to include "slotted" (keyword) arguments, the status of builtins, and support for imports.
The Rule Interchange Format (RIF) Working Group seeks public feedback on these Working Drafts. Please send your comments to public-rif-comments@w3.org (public archive). If possible, please offer specific changes to the text which will address your concern.
Publication as a Working Draft does not imply endorsement by the W3C Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress.
This document was produced by a group operating under the 5 February 2004 W3C Patent Policy. W3C maintains a public list of any patent disclosures made in connection with the deliverables of the group; that page also includes instructions for disclosing a patent. An individual who has actual knowledge of a patent which the individual believes contains Essential Claim(s) must disclose the information in accordance with section 6 of the W3C Patent Policy.
Based on the RIF Use Cases and Requirements, this document develops RIF-BLD (the Basic Logic Dialect of the Rule Interchange Format) through a set of foundational concepts that are intended to be shared by all logic-based RIF dialects. The overall RIF design takes the form of a layered architecture organized around the notion of a dialect.
A dialect is a rule language with a well-defined syntax and semantics. This semantics must be model-theoretic, proof-theoretic, or operational in this order of preference. Some dialects might be proper extensions of others (both syntactically and semantically) and some may have incompatible expressive power. RIF BLD has been designed to be extended by all future logic-based dialects
From a theoretical perspective, RIF-BLD corresponds to the language of definite Horn rules (see Horn Logic) with equality and with a standard first-order semantics. Syntactically, RIF-BLD has a number of extensions to support features such as objects and frames, internationalized resource identifiers (or IRIs, defined by RFC 3987) as identifiers for concepts, and XML Schema data types. These latter features make RIF a Web language. However, RIF is designed to enable interoperability among rule languages in general, and its uses are not limited to the Web. The semantics of RIF has provisions for future extensions towards dialects that support pure FOL, dialects that support negation as failure (NAF), business (or production) rules, reactive rules, and other features.
Eventually, it is hoped that RIF dialects will cover a number of important paradigms in rule-based specification and programming. Our main target paradigms include production rules, logic programming, FOL-based rules, reactive rules, and normative rules (integrity constraints).
The central part of RIF is its Condition Language. The condition language defines the syntax and semantics for the bodies of the rules in RIF-BLD and the syntax for queries. However, it is envisioned that the Condition Language will have wider use in RIF. In particular, it might be used as a sublanguage for specifying the conditional part in the bodies of production rules (RIF PRD), reactive rules, and normative rules.
As mentioned, IRI constants are used in RIF both as logical constants and as names for predicate and function symbols. RIF-BLD does not allow the same symbol to play more than one of these roles, but the dialects that extend RIF-BLD may support polymorphic symbols (i.e., symbols that have more than one contextual use; e.g., of a constant and of a predicate). Such polymorphism is common practice in Logic Programming (e.g., [Prolog], [F-logic], [HiLog]) and in [RDF]. This extensibility is achieved in RIF by building its syntax on the basis of signatures. This draft also introduces a frame-based syntax and semantics and defines a normative way for RIF rules to interact with RDF.
The current document is the second draft of the RIF-BLD specification (in the first draft called 'RIF Core'). A number of extensions are planned to support built-ins, additional primitive XML data types, the notion of RIF compliance, and so on. Tool support for RIF-BLD is forthcoming. RIF dialects that extend RIF-BLD will be specified in other documents by this working group.
The condition sublanguage of RIF-BLD is intended to be a common basis for the dialects of RIF. First of all, it is used by RIF-BLD itself. Future dialects or groups of dialects where the Condition Language or its extensions might be used include:
Rule bodies and queries in declarative logic programming dialects (LP)
Rule bodies in first-order dialects (FO)
Conditions in the rule bodies of the Production Rule Dialect (RIF PRD)
The event and condition parts of the rule bodies in reactive rule dialects (RR)
Integrity constraints (IC)
It should be noted, however, that apart from RIF-BLD and RIF-PRD no decision has been made regarding which dialects will ultimately be part of RIF.
The condition sublanguage of RIF-BLD is intended to be used only in rule bodies and queries, not in rule heads. The various RIF dialects diverge in the way they specify, interpret, or use the formulas that occur in their heads and in other components of the rules. By focusing on the condition part of the rule bodies we achieve a great deal of syntactic and semantic reuse among the dialects.
This part of the document describes Positive Conditions and Slotted Conditions.
The sublanguage of positive conditions in RIF-BLD determines what can appear as a body of a rule (also known as the if-part, antecedent, or condition part of the rule) supported by RIF-BLD. As explained in Section Overview, RIF-BLD corresponds to definite Horn rules, and the bodies of such rules are conjunctions of atomic formulas without negation. However, it is well-known that disjunctions of such conditions can also be used in the bodies of rules without changing the essential properties of the rule language. This is based on the fundamental logical tautologies (h ← b ∨ c) ≡ ((h ← b) ∧ (h ← c)) and ∀ x (F ∧ G) ≡ (∀ x F ∧ ∀ x G). In other words, a rule with a disjunction in the body can be split into two or more rules that have no such disjunction.
To make RIF dialects suitable as Web languages, RIF supports XML Schema primitive data types and some other data types. In addition, RIF promotes the use of Internationalized Resource Identifiers (or IRIs) RFC 3987 to refer to individuals, predicates, and functions.
To ensure extensibility and to provide for future higher-order dialects based on formalisms such as HiLog and Common Logic, RIF does not draw a sharp boundary between the symbols used to denote individuals from symbols used as names for functions or predicates. Instead, all constant, predicate, and function symbols are drawn from the same universal set. RIF dialects control the contexts in which the different symbols can occur by attaching signatures to these symbols.
RIF-BLD carefully selects signatures for the symbols so that the corresponding logic will be first-order: each symbol has a unique role as a symbol that represents an individual object, a function symbol of a particular arity, or a predicate symbol of a particular arity. However, dialects extending RIF-BLD will be allowed to use signatures in less restrictive fashions so that symbols could be polymorphic (i.e. be allowed to occur in several different contexts; e.g., as individuals and as predicates) and polyadic (i.e take a varying number of arguments).
We begin by describing a syntax, which is more general than what RIF-BLD permits. This syntax can be used in the various dialects that extend RIF-BLD. Then we introduce the notion of a signature and specify the restrictions on the way signatures are allowed to be assigned to symbols. Next we define the presentation syntax using EBNF and describe the corresponding XML-based exchange syntax. Finally, we give a model-theoretic semantics to RIF-BLD.
In this document we will introduce two related but distinct syntaxes:
Presentation syntax. This syntax is used in formal definitions, especially for the semantics. It is a human-oriented syntax and, therefore, we use it in the model theory and the examples. The presentation syntax is not meant to be used for exchange of RIF rules.
XML syntax. This syntax is the normative XML serialization of the presentation syntax. The key features of this syntax are derived from the presentation syntax, but some aspects related to rule exchange do not have counterparts in the presentation syntax.
The alphabet of RIF Condition Language consists of a countably infinite set of constant symbols Const, a countably infinite set of variable symbols Var (disjoint from Const), connective symbols And and Or, quantifier Exists, the symbol =, and auxiliary symbols, such as "(" and ")". In the RIF presentation syntax, variables are written as Unicode strings preceded with the symbol "?". The syntax for constant symbols is given in Section Symbol Spaces below.
The language of RIF-BLD is the set of formulas constructed using the above alphabet according to the rules spelled out below.
The basic language construct is called term, which is defined inductively as follows:
If t ∈ Const or t ∈ Var then t is a term.
If t and t_{1}, ..., t_{n} are terms then t ( t_{1} ... t_{n} ) is a term.
This definition is very general. It makes no distinction between constant symbols that represent individuals, predicates, and function symbols. The same symbol can occur in multiple contexts at the same time. For instance, if p, a, and b are symbols then p ( p ( a ) p ( a p c ) ) is a term. Even variables and general terms are allowed to occur in the position of predicates and function symbols, so p ( a ) ( ?v ( a c ) p ) is also a term. To control the context in which any given symbol can occur in a RIF dialect, the language associates a signature with each symbol (both constant and variable symbols).
Signatures. Let SigNames be a non-empty, partially-ordered finite or countably infinite set of signature names. We require that this set includes at least the name atomic, which represents the context of atomic formulas. Dialects are free to introduce additional signature names. For instance, as we shall soon see, RIF-BLD also introduces another signature, term{ }. The partial order on SigNames is dialect-specific (see, the specifics for RIF-BLD later); it is used in the definition of well-formed terms below.
We use the symbol < to represent the partial order on SigNames. Informally, α < β means that terms with signature α can be used wherever terms with signature β are allowed.
A signature is a statement of the form η{e_{1}, ..., e_{n}, ...} where η ∈ SigNames is the name of the signature and {e_{1}, ..., e_{n}, ...} is a countable set of arrow expressions. Such a set can thus be infinite, finite, or even empty. In RIF-BLD, signatures can have at most one arrow expression. Other dialects (such as HiLog, for example) may require polymorphic symbols and thus allow signatures with more than one arrow expression in them.
An arrow expression is defined as follows:
If κ, κ_{1}, ..., κ_{n}, n≥0, are signature names from SigNames, then (κ_{1} ... κ_{n}) ⇒ κ is an arrow expression. In particular, () ⇒ term and (term) ⇒ term are arrow expressions.
If κ above is atomic then the signature is called a Boolean expression.
A set S of signatures is coherent iff
S contains the special signature atomic{ }, which represents the context of atomic formulas; and
S has at most one signature for any given signature name.
Whenever S contains a pair of signatures, ηS and κR, such that η<κ then R⊆S. Here ηS denotes a signature with the name η and the associated set of arrow expression S; similarly κR is a signature named κ with the set of expressions R. The requirement that R⊆S ensures that symbols that have signature η can be used wherever the symbols with signature κ are allowed.
Signatures help control the context in which various symbols can occur through the notion of well-formed formulas. This is done using the notion of well-formed terms, as explained next.
Each constant and variable symbol is associated with exactly one signature from a coherent set of signatures. Different symbols can be associated with the same signature, but no symbol can be associated with more than one signature. The equality symbol, =, is also given a signature. This signature may vary from dialect to dialect, but RIF requires that it contains only the arrow expressions of the form (κ κ) ⇒ atomic (i.e., the arguments must have the same signature and the result must be atomic). Since signature names uniquely identify signatures in coherent signature sets, we will often use signature names to refer to signatures. For instance, we may say that symbol f has signature atomic rather than that "f has signature atomic{ }" or that "f has signature named atomic."
If s is a constant or variable symbol with signature η then s is a well-formed term with signature η.
A term t ( t_{1} ... t_{n} ), 0≤n, is a well-formed term whose signature is σ iff
t is a well-formed term that has a signature, which contains an arrow expression of the form (σ_{1} ... σ_{n}) ⇒ σ; and
Each t_{i} is a well-formed term whose signature is σ'_{i}, such that σ'_{i}, < σ_{i}.
As a special case, when n=0 we obtain that t ( ) is a well-formed term with signature σ, if t's signature contains the arrow expression () ⇒ σ.
A term t ( t_{1} ... t_{n} ) is a well-formed atomic formula iff it is a well-formed term with the signature atomic.
Since the signature of = contains only the arrow expressions of the form (κ κ) ⇒ atomic, it follows that an expression of the form t_{1} = t_{2} is a well formed term and also a well-formed atomic formula, only if t_{1} and t_{2} are well-formed terms that have the same signature.
Note that according to the above definition f ( ) and f are distinct terms.
More general formulas are constructed out of atomic formulas with the help of logical connectives. The condition sublanguage of RIF-BLD defines the following general well-formed condition formulas.
If φ is a well-formed atomic formula then it is also a well-formed condition formula.
If are φ_{1}, ..., φ_{n}, n ≥ 0, are well-formed condition formulas then so is And ( φ_{1} ... φ_{n} ). As a special case, And ( ) is allowed and is treated as a tautology true.
If φ_{1}, ..., φ_{n}, n ≥ 0, are well-formed condition formulas then so is Or ( φ_{1} ... φ_{n} ). When n=0, we get Or ( ) as a special case; it is treated as false -- a formula that is always false.
If φ is a well-formed condition formula and ?V_{1}, ..., ?V_{n} are variables then Exists ?V_{1} ... ?V_{n} ( φ ) is a well-formed condition formula.
Examples. We illustrate the above definitions with the following examples. In addition to atomic, the examples also use another signature, term{ }. As we shall soon see, this signature is used in RIF-BLD.
Consider the term p ( p ( a ) p ( a b c ) ). If p has the (polymorphic) signature mysig{(term)⇒term, (term term)⇒term, (term term term)⇒term} and a, b, c each has the signature term{ } then p ( p ( a ) p ( a b c ) ) is a well-formed term with signature term{ }. If instead p had the signature mysig2{(term term)⇒term, (term term term)⇒term} then p ( p ( a ) p ( a b c ) ) would not be a well-formed term since then p ( a ) would not be well-formed (in this case, p would have no arrow expression which allows p to take just one argument).
For a more complex example, let r have the signature mysig3{(term)⇒atomic, (atomic term)⇒term, (term term term)⇒term}. Then r ( r ( a ) r ( a b c ) ) is well-formed. The interesting twist here is that r ( a ) is a Boolean rather than an individual, but this is allowed by the arrow expression (atomic term)⇒ term, which is part of r's signature. If r's signature were mysig4{(term)⇒atomic, (atomic term)⇒atomic, (term term term)⇒term} instead, then r ( r ( a ) r ( a b c ) ) would be not only a well-formed term, but also a well-formed atomic formula.
An even more advanced example of using signatures is when the right-hand side of an arrow expression is something other than term or atomic. For instance, let John, Mary, NewYork, and Boston have signatures term{ }; flight and parent have signature h_{2}{(term term)⇒atomic}; and closure has signature hh_{1}{(h_{2})⇒p_{2}}, where the signature p_{2} has the form p_{2}{(term term)⇒atomic}. Then flight ( NewYork Boston ), closure ( flight ) ( NewYork Boston ), parent ( John Mary ), and closure ( parent ) ( John Mary ) would be well-formed formulas. Such formulas are allowed in languages like HiLog, which support predicate constructors like closure in the above example.
Throughout this document, the xsd: prefix stands for the XML Schema namespace URI http://www.w3.org/2001/XMLSchema#, the rdf: prefix stands for http://www.w3.org/1999/02/22-rdf-syntax-ns#, and rif: stands for the URI of the RIF namespace, http://www.w3.org/2007/rif#. Syntax such as xsd:string should be understood as a compact uri -- a macro that expands to a concatenation of the character sequence denoted by the prefix xsd and the string string. In the next version of this document we intend to introduce a syntax for defining prefixes for compact URIs.
The set of all constant symbols in RIF has a number of predefined subsets, called symbol spaces, which are used to represent XML Schema data types, data types defined in other W3C specifications, such as rdf:XMLLiteral, and to distinguish other sets of constants. Constant symbols that belong to the various symbol spaces have special presentation syntax and semantics.
Formally, a symbol space is a named subset of the set of all constants, Const. The semantic aspects of symbol spaces will be described in Section Model Theory for Condition Language of RIF BLD. Each symbol in Const belongs to a symbol space.
Each symbol space has an associated lexical space and a number of identifiers.
The lexical space of a symbol space is a non-empty set of Unicode character strings.
An identifier of a symbol space is an absolute IRI. The same symbol space is allowed to have more than one identifier (but different symbol spaces cannot share an identifier).
To simplify the language, this document will often use symbol space identifiers to refer to the actual symbol spaces (for instance, we may say "symbol space xsd:string" instead of "symbol space identified by xsd:string").
To refer to a constant in a particular RIF symbol space, we use the following presentation syntax:
LITERAL^^SYMSPACE
where LITERAL is a Unicode string, called the lexical part of the symbol, and SYMSPACE is an identifier of the symbol space in the form of an absolute IRI string. LITERAL must be an element in the lexical space of the symbol space. For instance, 1.2^^xsd:decimal and 1^^xsd:decimal are legal symbols because 1.2 and 1 are members of the lexical space of the XML Schema data type xsd:decimal. On the other hand, a+2^^xsd:decimal is not a legal symbol, since a+2 is not part of the lexical space of xsd:decimal.
RIF-compliant implementations must support the following symbol spaces. Rule sets that are exchanged through RIF can use additional symbol spaces as explained below.
xsd:long (http://www.w3.org/2001/XMLSchema#long).
xsd:string (http://www.w3.org/2001/XMLSchema#string).
xsd:integer (http://www.w3.org/2001/XMLSchema#integer).
xsd:decimal (http://www.w3.org/2001/XMLSchema#decimal).
xsd:time (http://www.w3.org/2001/XMLSchema#time).
xsd:dateTime http://www.w3.org/2001/XMLSchema#dateTime).
The lexical spaces of the above symbol spaces are defined in the document XML Schema Part 2: Datatypes.
rdf:XMLLiteral (http://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral).
This symbol space represents XML content. The lexical space of rdf:XMLLiteral is defined in the document Resource Description Framework (RDF): Concepts and Abstract Syntax.
rif:text (for text strings with language tags attached).
This symbol space represents text strings with a language tag attached. The lexical space of rif:text is the set of all Unicode strings of the form ...@LANG, i.e., strings that end with @LANG where LANG is a language identifier as defined in IETF RFC 3066.
rif:iri (for internationalized resource identifier or IRI).
Constant symbols that belong to this symbol space are intended to be used in a way similar to RDF resources. The lexical space consists of all absolute IRIs as specified in RFC 3987; it is unrelated to the XML primitive type anyURI. A rif:iri constant is supposed to be interpreted as a reference to one and the same object regardless of the context in which that constant occurs.
rif:local (for constant symbols that are not visible outside of a particular set of RIF formulas).
Symbols in this symbol space are used locally in their respective rule sets. This means that occurrences of the same rif:local-constant in different rule sets are viewed as unrelated distinct constants, but occurrences of the same constant in the same rule set must refer to the same object. The lexical space of rif:local is the same as the lexical space of xsd:string.
Symbols with an ill-formed lexical part. RIF constant symbols that belong to one of the aforesaid RIF-supported symbol spaces must be well-formed, i.e., their lexical part must belong to the lexical space associated with the symbol space. For instance, 123^^xsd:long has a correct lexical part, since 123 belongs to the lexical space of the data type xsd:long. In contrast, abc^^xsd:long is ill-formed, as it does not have a correct lexical part. A compliant RIF-BLD interpreter must reject ill-formed symbols.
Symbols with undefined symbol spaces. RIF allows symbols of the form LITERAL^^SYMSPACE where SYMSPACE is not one of the pre-defined RIF symbol spaces. These are treated as "uninterpreted" constant symbols in the RIF language and the lexical space of such a symbol space is considered to be the set of all Unicode strings. Dialects that extend RIF-BLD might appropriate some of the symbol spaces, which are left undefined in RIF-BLD, and give them special semantics.
RIF-BLD presents a much simpler picture to the user by restricting the set of well-formed terms to a specific coherent set of signatures. Namely, the signature set of RIF-BLD contains the following signatures:
term{ }, atomic{ }, bi_atomic{ }, where bi_atomic<atomic.
The signature term{ } represents the context in which individual objects (but not atomic formulas) can appear. The signature bi_atomic{ } represents atomic formulas for builtin predicates (such as fn:substring). Since bi_atomic<atomic, builtin atomic formulas are also atomic formulas, but normally most atomic formulas are user-defined and they will have the signature atomic rather than bi_atomic.
For every integer n ≥ 0, there are signatures f_{n}{(term ... term) ⇒ term}, p_{n}{(term ... term) ⇒ atomic}, and bi_{n}{(term ... term) ⇒ bi_atomic} (in each case there are n terms inside the parentheses), which represent function symbols of arity n, (user-defined) predicate symbols of arity n, and n-ary builtin predicates, respectively. The symbols f_{n} p_{n}, and bi_{n} are reserved signature names in RIF-BLD.
A symbol in Const can have exactly one signature, f_{n}, p_{n}, or bi_{n}, where n ≥ 0. It cannot have the signature atomic or bi_atomic (only terms can have such signatures, not symbols). Thus, in RIF-BLD each constant symbol can be either an individual, a predicate of one particular arity, 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 RIF-BLD. The symbols of type rif:iri and rif:local can have the following signatures in RIF-BLD: term, f_{n}, p_{n}, or bi_{n}, for n = 0,1,....
All variables are associated with signature term{ }, so they can range only over individuals.
A equality formula, =, has signature p_{2}{(term term) ⇒ atomic}. This means that equality can compare only those terms whose signature is term; it cannot compare predicate names or function symbols.
RIF-BLD requires no extra syntax for declaring signatures, since signatures can be inferred. Indeed, RIF-BLD requires that each symbol is associated with a unique signature. Therefore, 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 uniterms and atomic formulas are guaranteed to be well-formed. As a consequence, signatures are not part of the RIF-BLD language and term, atomic, and bi_atomic are not reserved keywords.
Builtin predicates are not subject to the above signature inference rule. The signatures of the builtin predicates are defined by List_of_functions_and_operators. In particular, all symbols with the http://www.w3.org/2005/xpath-functions# prefix are considered to be builtins and have signatures of the form bi_{n}{... ⇒ bi_atomic}.
In dialects that extend RIF-BLD, signature inference may not always be possible. We expect that most dialects will use signature inference and RIF does not define any special sublanguage for signatures. However, signature inference may not always be possible or desirable in some dialects. In these cases, we expect those dialects to introduce their own primitives for defining signatures.
The overall structure of the syntax used in the RIF-BLD condition sublanguage is depicted on the following diagram.
The central syntactic class of RIF, CONDITION, is specified recursively through its subclasses and their parts. The Equal class has two side roles. Two pairs of roles distinguish between the declare and formula parts of the Exists class, and between the operation (op) and arguments (arg) of the Uniterm class, where multiple arguments are subject to an ordered constraint (the natural "left-to-right" order).
The syntactic classes are partitioned into classes that will not be visible in serializations (written in all-uppercase letters) and classes that will be visible in instance markup (written with a leading uppercase letter only).
The three classes Var, CONDITION, and ATOMIC are used in the syntax of Horn Rules.
We now give an EBNF for the RIF presentation syntax. This syntax is somewhat abstract in nature. In particular, it does not address the concrete details of how constants and variables are represented. For instance, it ignores the issues that have to do with delimiters, such as white spaces and escape symbols. Instead, white space is informally used as a delimiter. For instance, TERM* is to be understood as TERM* ::= | TERM TERM*. This is done on purpose, since RIF's presentation syntax is intended to be used for specifying semantics and to illustrate the main RIF concepts through examples. It is not intended as a concrete syntax for a rule language. RIF defines a concrete syntax only for exchanging rules, and that syntax is XML-based.
EBNF grammar CONDITION ::= 'And' ' ( ' CONDITION* ' ) ' | 'Or' ' ( ' CONDITION* ' ) ' | 'Exists ' Var+ ' ( ' CONDITION ' ) ' | ATOMIC ATOMIC ::= Uniterm | Equal Uniterm ::= Const ' ( ' TERM* ' ) ' Equal ::= TERM ' = ' TERM TERM ::= Const | Var | Uniterm Const ::= LITERAL '^^' SYMSPACE Var ::= '?' VARNAME
The above is a standard syntax for a variant of first-order logic. The application of a constant (Const) symbol to a sequence of terms is called a Uniterm (Universal term); it can play the role of a term or an atomic formula depending on the syntactic context in which the application occurs. The non-terminal ATOMIC stands for atomic formula. The Exists formula, where Var+ stands for the list of variables that are free in CONDITION, is an existential formula. It is the only kind of quantified formulas in RIF-BLD, but other dialects may add universal quantification. The And formula defines conjunctions of conditions, and 'Or' denotes disjunctions. Finally, CONDITION assembles everything into what we earlier called RIF condition formulas.
Note that individuals, function symbols, and predicate symbols all belong to the same set of symbols Const. This syntax is more general than what RIF-BLD actually permits. As explained in Section Symbols and Signatures a set of signatures further restricts this syntax to allow only the standard first-order logic terms.
RIF-BLD presentation syntax does not commit to any particular vocabulary for the names of variables or for the literals used in constant symbols. In the examples, variables are denoted by Unicode character sequences beginning with a ?-sign. Constant symbols have the form: LITERAL^^SYMSPACE, where SYMSPACE is an IRI string that identifies the symbol space of the constant and LITERAL is a Unicode string from the lexical space of that symbol space.
In the condition language of RIF-BLD, a variable can be free or quantified. All quantification is explicit and the variables introduced by quantification must also occur in the quantified formula. Variables that are not explicitly quantified are free.
Conditions with free variables are used as queries and also in the if part of a rule. In the latter case, the free variables in a condition formula must also occur in the then part of the rule. We shall see in Section Horn Rules that such variables are quantified universally outside of the rule, and the scope of such quantification is the entire rule. For instance, the variable ?Y in the first RIF condition of Example 1 is quantified, existentially, but ?X is free. However, when this condition occurs in the if part of the second rule in Example 1, then this variable is quantified universally outside of the rule. (The precise syntax for RIF rules is given in Section Horn Rules.)
Example 1 (A RIF condition in and outside of a rule) RIF condition: Exists ?Y ( condition ( ?X ?Y ) ) RIF Horn rule: Forall ?X ( then_part ( ?X ) :- Exists ?Y ( condition ( ?X ?Y ) ) )
The XML serialization for RIF-BLD presentation syntax given in this section is alternating or fully striped (e.g., Alternating Normal Form). Positional information is optionally exploited only for the arg role elements. For example, role elements (declare and formula) are explicit within the Exists element. Following the examples of Java and RDF, we use capitalized names for class elements and names that start with lowercase for role elements.
The all-uppercase classes in the presentation syntax, such as CONDITION, become XML entities. They act like macros and are not visible in instance markup. The other classes as well as non-terminals and symbols (such as Exists or =) become XML elements with optional attributes, as shown below.
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 (atomic or function-expression formula) - op (operation role) - arg (argument role) - Equal (prefix version of term equation '=') - side (left-hand and right-hand side role) - Const (predicate symbol, function symbol, or individual, with optional 'type' attribute) - Var (logic variable)
For the XML Schema Definition (XSD) of the RIF-BLD condition language see Appendix Specification.
The XML syntax for symbol spaces utilizes the type attribute associated with XML term elements such as Const. For instance, a literal in the xsd:dateTime data type can be represented as <Const type="xsd:dateTime">2007-11-23T03:55:44-02:30</Const>.
The following example illustrates XML serialization of RIF conditions.
Example 2 (A RIF condition and its XML serialization): We use the prefix bks as an abbreviation for http://example.com/books# and curr for http://example.com/currencies# a. RIF condition And ( Exists ?Buyer ( purchase^^rif:local ( ?Buyer ?Seller book^^rif:local ( ?Author bks:LeRif^^rif:iri ) curr:USD^^rif:iri ( 49^^xsd:integer ) ) ?Seller=?Author ) b. XML serialization <And> <formula> <Exists> <declare><Var>Buyer</Var></declare> <formula> <Uniterm> <op><Const type="rif:local">purchase</Const></op> <arg><Var>Buyer</Var></arg> <arg><Var>Seller</Var></arg> <arg> <Uniterm> <op><Const type="rif:local">book</Const></op> <arg><Var>Author</Var></arg> <arg><Const type="rif:iri">bks:LeRif</Const></arg> </Uniterm> </arg> <arg> <Uniterm> <op><Const type="rif:iri">curr:USD</Const></op> <arg><Const type="xsd:integer">49</Const></arg> </Uniterm> </arg> </Uniterm> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And>
The translation between the presentation syntax and the XML syntax 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> |
left = right | <Equal> <side>left</side> <side>right</side> </Equal> |
name^^space | <Const type="space">name</Const> |
?name | <Var>name</Var> |
The first step in defining a model-theoretic semantics for a logic-based language is to define the notion of a semantic structure, also known as an interpretation. (See end note on the rationale.) In this section we define basic semantic structures. This definition will be extended in Extension of Semantic Structures for Frames when we introduce frame syntax.
Semantic structures are used to assign a truth value to each formula. Currently, by formula we mean anything produced by the CONDITION production in the presentation syntax. Later on, formulas will also include rules. We first define the notion of a truth value formally and then introduce semantic structures. Next we give the semantics to symbol spaces and, finally, define truth values of formulas with respect to semantic structures.
Truth values. The set of truth values is denoted by TV. For RIF-BLD, TV includes only two values, t (true) and f (false). (See end note on truth values.)
In RIF, TV has a total or partial order, called the truth order, and denoted with <_{t}. In RIF-BLD, f <_{t} t, and it is a total order. (See end note on ordering truth values.)
Semantic structures. A basic semantic structure, I, is a tuple of the form <D,I_{C}, I_{V}, I_{F}, I_{R}>.
Here D is a non-empty set of elements called the domain of interpretation of I. We will continue to use Const to refer to the set of all constant symbols and Var to refer to the set of all variable symbols.
The other components of I are mappings defined as follows:
I_{C} from Const to elements of D
I_{V} from Var to elements of D
I_{F} from Const to functions from D* into D (here D* is a set of all tuples of any length over the domain D)
I_{R} from Const to truth-valued mappings D* → TV
We also define the following mapping, I, based on the mappings I_{C}, I_{V}, and I_{F}:
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}(f)(I(t_{1}),...,I(t_{n}))
Semantics of symbol spaces. Symbol spaces affect the domain of I and the mapping I_{C} as follows. First, some symbol spaces, called primitive data types, have a value space, denoted VS_{symsp}, and a mapping from the lexical space to the VS_{symsp}, denoted L_{symsp}, where symsp is an identifier for the symbol space.
The value space and the lexical-to-value-space mapping are defined as part of the data type definition and do not depend on I. For every primitive datatype symsp it must hold that:
VS_{symsp} ⊆ D; and
For each constant lit^^symsp in the symbol space symsp, I_{C}(lit^^symsp) = L_{symsp}(lit).
That is, when restricted to a symbol space, symsp, I_{C} must map the corresponding constants according to L_{symsp}.
RIF-BLD does not impose restrictions on the interpretation of constants (the mapping I_{C}) in symbol spaces which are not primitive datatypes. Other dialects may do so. An example of such a restriction is that no constant in a particular symbol space may be mapped to an element in the value space of any XML Schema data type.
The above semantics is not limited to any particular set of symbol spaces or primitive data types. Any symbol space is covered as long as its lexical space is well-defined, and any data type is acceptable as long as its value space and the lexical-to-value mapping are known.
The primitive data types that are currently supported by RIF, xsd:long, xsd:integer, xsd:decimal, xsd:string, xsd:time, and xsd:dateTime, rdf:XMLLiteral, and rif:text, are required to be covered by every interpretation. Their value spaces and the lexical-to-value space mappings are defined as follows:
For XML Schema data types (xsd:long, xsd:integer, xsd:decimal, xsd:string, xsd:time, and xsd:dateTime), these are defined in the XML Schema Part 2: Datatypes specification.
The value space for the primitive data type rdf:XMLLiteral is defined in Resource Description Framework (RDF): Concepts and Abstract Syntax.
The value space of rif:text is the set of all pairs of the form (string, lang), where string is a Unicode character sequence and lang is a lowercase Unicode character sequence which is a natural language identifier as defined by RFC 3066. The lexical-to-value mapping of rif:text, L_{rif:text}, maps each symbol string@lang in the lexical space of rif:text to (string, lower-case(lang)), where lower-case(lang) is lang written in all-lowercase letters.
The value space and the lexical-to-value mapping for rif:text defined here are compatible with RDF's semantics for strings with named tags.
The value space of a data type should not be confused with the lexical space. Lexical spaces define the syntax of the constant symbols that belong to the various primitive data types. In contrast, value spaces define the meaning of the constants in data types. The lexical and the value spaces are often not even isomorphic. For instance, 1.2^^xsd:decimal and 1.20^^xsd:decimal are two legal constants in RIF because 1.2 and 1.20 belong to the lexical space of xsd:decimal. However, these two constants are interpreted by the same element of the value space of the xsd:decimal type. Therefore, 1.2^^xsd:decimal = 1.20^^xsd:decimal is a RIF tautology. Likewise, RIF semantics for data types implies certain inequalities. For instance, abc^^xsd:string ≠ abcd^^xsd:string is a tautology, since I_{C} must map these two constants into distinct elements in the value space of xsd:string. On the other hand, abc^^rif:local ≠ abcd^^rif:local is not a tautology in RIF, since I_{C} is not restricted over the lexical space of rif:local and these two constants can be mapped to the same element in D in some semantic structures and to different elements in others.
Semantics of undefined symbol spaces. Section Symbol Spaces addressed the syntactic aspects of the treatment of "unknown" symbol spaces, i.e., symbol spaces that are not defined by the RIF specification. It defined the lexical space of those symbols as the set of all Unicode strings. Semantically, unknown symbol spaces are treated as follows. First, they are not assigned any value space. Thus, such symbol spaces are not considered to be primitive data types by RIF even though they may be viewed as data types by some concrete rule languages that use RIF for exchange. Second, RIF does not impose any restrictions on the mapping I_{C} over the unknown symbol spaces.
Truth valuation of formulas. Observe that the notion of signatures from Section Symbols and Signatures is used only to constrain the syntax and does not appear in the definition of the semantic structure. This is because when we define truth valuations for formulas, below, all formulas are assumed to be well-formed.
Truth valuation for well-formed formulas in RIF-BLD is determined using the following function, denoted I_{Truth}:
Atomic formulas: I_{Truth}(r ( t_{1} ... t_{n} )) = I_{R}(r)(I(t_{1}),...,I(t_{n}))
Equality: I_{Truth}(t_{1} = t_{2}) = t iff I(t_{1}) = I(t_{2}); I_{Truth}(t_{1}=t_{2}) = f otherwise.
Conjunction: I_{Truth}(And ( c_{1} ... c_{n} )) = min_{t}(I_{Truth}(c_{1}),...,I_{Truth}(c_{n})), where min_{t} is minimum with respect to the truth order.
Disjunction: I_{Truth}(Or ( c_{1} ... c_{n} )) = max_{t}(I_{Truth}(c_{1}),...,I_{Truth}(c_{n})), where max_{t} is maximum with respect to the truth order.
Quantification: I_{Truth}(Exists ?v_{1} ... ?v_{n} ( c )) = max_{t}(I*_{Truth}(c)), where max_{t} is taken over all interpretations I* of the form <D,I_{C}, I*_{V}, I_{F}, I_{R}>, where the mapping I*_{V} has the same value as I_{V} on all variables except, possibly, on the variables ?v_{1},...,?v_{n}.
In this section we extend Positive Conditions, defined in Section Positive Conditions, with slotted Uniterms and Frame formulas. A slot can be represented by an individual symbol or, more generally, by a Uniterm. It can be represented by an IRI or be known only locally. Semantically, a frame slot is a set-valued function that represents a property of an object. Such a function maps an object id to a set of values of the property. This can be a singleton set or even an empty set. In contrast, a uniterm slot semantically behaves like a unary uninterpreted function symbol. In both cases, however, the order of the slots is immaterial (in contrast to positional uniterms).
Syntactically, the extension is achieved by extending the notion of a uniterm with slots and by adding a new kind of formula, called frame formula. For uniformity and greater syntactic convenience, frame formulas can be nested inside other frame formulas. However, this feature is just a syntactic sugar that does not extend the expressive power.
The alphabet of the language is extended with symbols ->, #, and ##, and the language of positive conditions in Section Symbols and Signatures is extended with slotted terms, slotted predicates, and frames.
Slotted terms. A term is either a term in the sense of Section Symbols and Signatures or a slotted term.
A slotted term is of the form t ( p_{1} -> v_{1} ... p_{n} -> v_{n} ), where t is a term; p_{1}, ..., p_{n} are terms, which represent the names of the slots; and v_{1} , ..., v_{n} are terms. Slotted terms are like regular terms except that the arguments are named and their order is considered to be immaterial.
In order to talk about the slotted terms that are also well-formed, we need to extend the notion of a signature to include slots. As before, a slotted signature is a statement of the form η{e_{1}, ..., e_{n}, ...} where η ∈ SigNames is the name of the signature and {e_{1}, ..., e_{n}, ...} is a countable set of slotted arrow expressions. A slotted arrow expression is a statement of the form
(γ_{1} -> κ_{1}, ..., γ_{n} -> κ_{n}) => κ, where n≥0. The order of the arguments in a slotted arrow expression is assumed to be immaterial, so any permutation of arguments is assumed to yield the same expression. For instance, (term -> term, term -> term) => term is a slotted arrow signature expression. By analogy with earlier definitions, if κ is atomic then the expression is also a slotted Boolean expression. For instance, (term -> term, term -> term) => atomic is a slotted Boolean signature expression.
A term t ( p_{1} -> v_{1} ... p_{n} -> v_{n} ) is a well-formed slotted term with signature σ if
Each p_{i} is a well-formed term with some signature γ_{i}.
Each v_{i} is a well-formed term (slotted or non-slotted) with some signature σ_{i}, i=1, ..., n.
The signature of t includes a slotted arrow expression of the form (γ_{1} -> σ_{1} ... γ_{n} -> σ_{n}) => σ.
The aforesaid term t is a well-formed slotted atomic formula if σ is atomic.
A slotted atomic formula is just like an atomic formula of Section Symbols and Signatures except that the arguments of the predicate are named and their order is considered immaterial. This is analogous to names of columns in tables in relational databases.
Editor's Note: The use of slotted terms is an open issue in the current draft http://www.w3.org/2005/rules/wg/track/issues/44.
Frames. A well-formed frame formula is one of the following:
Membership formula: Depending on the dialect, the symbol # can have different signatures, but they can contain only the arrow expression of the form (κ_{1} κ_{2}) ⇒ atomic. A membership formula o # c is well-formed and has the signature atomic, if o, c are well-formed terms that have the signatures κ_{1} and κ_{2}, respectively.
Informally, such a formula says that object o is a member of class c. A RIF class is an object, which can have other classes as members, as specified by membership formulas. Thus, classes are also objects and they can be members of some other classes. (In object-oriented languages these latter classes are sometimes known as meta-classes.)
Subclass formula: Depending on the dialect, the symbol ## can have different signatures, but they can contain only the arrow expression of the form (κ κ) ⇒ atomic. A subclass formula s ## c is well-formed and has the signature atomic, if s and c are well-formed terms with signature κ.
Informally, this formula states that class s is a subclass of class c. Note that both arguments must have the same signature, since the subclass relationship is supposed to be transitive.
Frame: t [ p_{1} -> v_{1} ... p_{n} -> v_{n} ], where t is a well-formed term, a membership formula, or a subclass formula; p_{1}, ..., p_{n} are well-formed terms; and each v_{1} , ..., v_{n} is either a well-formed term or a well-formed frame formula.
When t, all the p_{i}, and all the v_{i} are terms, such a formula should be understood as a statement that object t has properties p_{i}, ..., p_{n}, and for each i = 1,...,n, the value of property p_{i} is a set that contains the object v_{i}. When t, p_{i}, or v_{i} are not just terms but frame formulas themselves, the above is treated as a conjunction of simpler frame formulas, as defined by the unnest transformation in the section on semantics (below).
Editor's Note: The use of membership and subclass formulas is an open issue in the current draft http://www.w3.org/2005/rules/wg/track/issues/41.
Atomic formulas and general condition formulas. The syntax for atomic formulas is extended with slotted formulas and frame formulas. More precisely, an atomic well-formed formula is
An atomic well-formed formula as defined in Section Symbols and Signatures; or
The notion of well-formed condition formulas needs no adjustments with respect to the earlier definition (without frames or slots). As before, such formulas are constructed from well-formed atomic formulas using the logical connectives And, Or, and the quantifier Exists.
Slotted signatures for RIF-BLD. Section Symbols and Signatures defined the allowed signatures for RIF-BLD. With the introduction of slotted signatures, we add the following signatures to those already defined for RIF-BLD:
For every n≥0 there are signatures fs_{n}{(term -> term, ..., term -> term) => term} and ps_{n}{(term -> term, ..., term -> term) => atomic} (in both cases the number of arguments inside the parentheses is n).
In addition, RIF-BLD imposes the following restrictions:
must have the signature term{ }; and
In frame formulas, all terms must have the signature term and #, ## must have the signature p_{2}{(term term)⇒atomic}.
Therefore, in the frame formulas t # s, t ## s, or t [ r -> s ], the terms t, s, and r cannot have the signature atomic -- they can represent individuals, but not predicates.
We now extend the presentation syntax of Positive Conditions to a presentation syntax for slotted terms and frames.
EBNF grammar CONDITION ::= 'And' ' ( ' CONDITION* ' ) ' | 'Or' ' ( ' CONDITION* ' ) ' | 'Exists' Var+ ' ( ' CONDITION ' ) ' | ATOMIC ATOMIC ::= Uniterm | Equal | CLASSIFICATION | Frame Uniterm ::= Const ' ( ' (TERM* | (Const ' -> ' TERM)*) ' ) ' Equal ::= TERM '=' TERM CLASSIFICATION ::= TERM ' # ' TERM | TERM ' ## ' TERM Frame ::= (TERM | CLASSIFICATION) ' [ ' (TERM ' -> ' (TERM | Frame))* ' ] ' TERM ::= Const | Var | Uniterm Const ::= LITERAL '^^' SYMSPACE Var ::= '?' VARNAME
A Uniterm applies a symbolic constant (from Const) to positional TERM arguments or to slotted Const -> TERM arguments. A CLASSIFICATION specifies that one object is a member (in case of the #-connective) or a subclass (in case of the ##-connective) of another object. A Frame is a TERM or a CLASSIFICATION applied to slotted TERM -> (TERM | Frame) arguments.
Example 3 shows Uniterm and Frame conditions, the latter with variables for the three major (combinations of) syntactic categories, corresponding to the three components of RDF triples.
Example 3 (A RIF condition with bound variables) We use the prefix bks to abbreviate http://example.com/books# and the prefix auth for http://example.com/authors#. RIF conditions using Positional Uniterms: book^^rif:local ( auth:rifwg^^rif:iri bks:LeRif^^rif:iri ) Exists ?X ( book^^rif:local ( ?X LeRif^^rif:local ) ) Slotted Uniterms: book^^rif:local ( author^^rif:local -> auth:rifwg^^rif:iri title^^rif:local -> bks:LeRif^^rif:iri ) Exists ?X ( book^^rif:local ( author^^rif:local -> ?X title^^rif:local -> bks:LeRif^^rif:iri ) ) Frames: wd1^^rif:local [ author^^rif:local -> auth:rifwg^^rif:iri title^^rif:local -> bks:LeRif^^rif:iri ] Exists ?X ( wd2^^rif:local [ author^^rif:local -> ?X title^^rif:local -> bks:LeRif^^rif:iri ] ) Exists ?X ( wd2^^rif:local # book^^rif:local [ author^^rif:local -> ?X title^^rif:local -> bks:LeRif^^rif:iri ] ) Exists ?I ?X ( ?I [ author^^rif:local -> ?X title^^rif:local -> bks:LeRif^^rif:iri ] ) Exists ?I ?X ( ?I # book^^rif:local [ author^^rif:local -> ?X title^^rif:local -> bks:LeRif^^rif:iri ] ) Exists ?S ( wd2^^rif:local [ author^^rif:local -> auth:rifwg^^rif:iri ?S -> bks:LeRif^^rif:iri ] ) Exists ?X ?S ( wd2^^rif:local [ author^^rif:local -> ?X ?S -> bks:LeRif^^rif:iri ] ) Exists ?I ?X ?S ( ?I # book^^rif:local [ author -> ?X ?S -> bks:LeRif^^rif:iri ] )
The following is an XML-serializing mapping of the presentation syntax in Section EBNF for the Presentation Syntax, extending the one in Section Positive Conditions.
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 (positional or slotted Uniterm formula) - Member (member formula) - Subclass (subclass formula) - Frame (Frame formula) - object (Member/Frame role containing a TERM or an object description) - op (Uniterm function/predicate role) - upper (Member/Subclass upper class role) - lower (Member/Subclass lower instance/class role) - slot (Uniterm/Frame slot role, prefix version of slot infix ' -> ') - Equal (prefix version of term equation '=') - side (Equal left-hand and right-hand side role) - Const (slot, individual, function, or predicate symbol) - Var (logic variable)
For the XML Schema Definition (XSD) of the RIF-BLD slotted condition language see Appendix Specification.
The following example illustrates XML serialization of Slotted RIF conditions.
Example 4 (A RIF condition and its XML serialization): We use the prefix bks to abbreviate http://example.com/books#, the prefix auth for http://example.com/authors#, and curr for http://example.com/currencies#, a. RIF condition: And ( Exists ?Buyer ?P ( ?P # purchase^^rif:local [ buyer^^rif:local -> ?Buyer seller^^rif:local -> ?Seller item^^rif:local -> book^^rif:local ( author^^rif:local -> ?Author title^^rif:local -> bks:LeRif^^rif:iri ) price^^rif:local -> 49^^xsd:integer currency^^rif:local -> curr:USD^^rif:iri ] ) ?Seller=?Author ) b. XML serialization: <And> <formula> <Exists> <declare><Var>Buyer</Var></declare> <declare><Var>P</Var></declare> <formula> <Frame> <object> <Member> <lower><Var>P</Var></lower> <upper><Const type="rif:local">purchase</Const></upper> </Member> </object> <slot><Const type="rif:local">buyer</Const><Var>Buyer</Var></slot> <slot><Const type="rif:local">seller</Const><Var>Seller</Var></slot> <slot> <Const type="rif:local">item</Const> <Uniterm> <op><Const type="rif:local">book</Const></op> <slot><Const type="rif:local">author</Const><Var>Author</Var></slot> <slot><Const type="rif:local">title</Const><Const type="rif:iri">bks:LeRif</Const></slot> </Uniterm> </slot> <slot><Const type="rif:local">price</Const><Const type="xsd:integer">49</Const></slot> <slot><Const type="rif:local">currency</Const><Const type="rif:iri">curr:USD</Const></slot> </Frame> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And>
The translation from the presentation syntax to the XML syntax is given by a table, below, which extends the translation table of Positive Conditions.
Presentation Syntax | XML Syntax |
---|---|
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> |
The syntax of RIF frames permits nesting of two kinds. First, a classification formula of the form obj1 # obj2 or obj1 ## obj2 can appear in the object position of a frame. Second, a frame may appear in the value position of a slot. This nested notation is convenient and allows succinct representation of object properties, but is no more than a shorthand notation. A nested frame represents a conjunction of flat frames. For instance,
a # b [ c -> e ## f [ g -> h ] ] = And ( a # b a [ c -> e ] e ## f e [ g -> h ] )
Formally, given a frame, f, we define the Unnest transformation and postulate f to be true in a semantic structure iff Unnest(f) is true. In this way, we reduce the semantics of nested frames to that of flat frames. Then we extend the basic semantic structures defined in Model Theory for the Core RIF Condition Language and define an interpretation for flat frames. The rest of the semantic definition does not change, since it is defined in terms of atomic formulas (the ATOMIC production in the BNF syntax).
If a formula, f, has the form a # b or a ## b then define Obj(f) to be a. If f has the form o [ a -> v ], where o, a, and v are terms, then Obj(f) is defined to be Obj(o). If f is a term then Obj(f) = f. Now, if f is a term then we define Unnest(f) = true, where true is a formula that is always true (a tautology). If f is a classification formula then Unnest(f) = f. Otherwise, if f is a frame of the form o [ a -> v ] then
Unnest(f) = And(Unnest(o) Obj(o) [ a -> Obj(v) ] Unnest(v))
For instance, in case of the frame a # b [ c -> e ## f [ g -> h ] ] above, unnesting yields:
Unnest(a # b [ c -> e ## f [ g -> h ] ]) = And(a # b a [ c -> e ] e ## f e [ g -> h ] true)
This is almost the same conjunction as we have seen earlier. The only difference is the trailing true conjunct, which comes from Unnest(h) and can be omitted.
A semantic structure, I, is a tuple of the form
<D,I_{C}, I_{V}, I_{F}, I_{R}, I_{slot}, I_{SF}, I_{SR}, I_{sub}, I_{isa}>.
All the components except the last five, I_{slot}, I_{SF}, I_{SR}, I_{sub}, I_{isa}, are the same as before. The new mapping I_{slot} is used to interpret frames; the mappings I_{SF} and I_{SR} interpret terms and predicates with named arguments, respectively; I_{sub} gives meaning to the subclass hierarchy; and I_{isa} interprets class membership.
I_{slot} is a function from the domain D to truth-valued functions of the form D × D → TV. The intuitive meaning of frame slots is that they are functions that take objects and return sets of objects, where every member of the set has a certain degree of truth. In the two-valued case, a set of objects associated with the truth value true represents the (set of) values that the slot returns when applied to an object. Formally, this is expressed by extending I_{Truth} to flat frames as follows:
I_{Truth}(T [ p_{1} -> V_{1} ... p_{k} -> V_{k} ]) = min_{i=1...k}(I_{Truth}(T [ p_{i} -> V_{i} ])), where T, p_{i}, and V_{i} are terms.
I_{Truth}(T [ p -> V ]) = I_{slot}(I(p))(I(T),I(V))
I_{SF} interprets terms with named arguments. It is a function from Const to the mappings SetOfFiniteSubbags(D × D) → D. This is analogous to the interpretation of regular (positional) terms with two differences:
Each argument <s,v> ∈ D × D represents a slot-name/slot-value pair instead of just a value in positional terms.
Bags are used here because, for slotted terms, the order of slot/value pairs is immaterial, but sets cannot be used, since I may happen to map different slots into the same value in D.
We can now extend the mapping I from Section Model Theory for Condition Language of RIF BLD as follows (where only the last item is new with respect to the earlier definition of 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}(f)(I(t_{1}),...,I(t_{n}))
I(f ( p_{1} -> t_{1} ... p_{n} -> t_{n} )) = I_{SF}(f)({<I(p_{1}),I(t_{1})>,...,<I(p_{n}),I(t_{n})>})
I_{SR} is used to interpret predicates with slotted
arguments. It is a function from Const to truth-valued mappings SetOfFiniteSubbags(D × D) → TV. This is analogous to the interpretation of regular (positional) predicates except for two differences:
Each pair <s,v> ∈ D × D represents a slot-name/slot-value pair instead of just a value in positional predicates.
Bags (also known as multisets) are used here because for slotted predicates the order of slot-value pairs does not matter, but sets cannot be used, since I may happen to map different slots into the same value in D.
We can now define I_{Truth} for slotted predicates as follows:
I_{Truth}(p ( p_{1} -> val_{1} ... p_{k} -> val_{k} )) = I_{SR}(p)({<I(p_{1}) I(val_{1})>, ... , <I(p_{k}) I(val_{k})>}), where p, p_{i} ∈ Const and val_{i} is a term for i=1,...k.
I_{sub} gives meaning to the subclass relationship. It is a truth-valued function D × D → TV. The truth valuation for classification formulas of the form sc ## cl, where sc and cl are terms, is defined as follows:
I_{Truth}(sc ## cl) = I_{sub}(I(sc), I(cl))
In addition, we want the operator ## to be transitive, i.e., we would like c1 ## c2 and c2 ## c3 to imply c1 ## c3. To this end, we require that the mapping I_{sub} defines a partial order on D. More precisely,
For all elements ec1, ec2, ec3 ∈ D, the following must hold: min_{t}(I_{sub}(ec1, ec2), I_{sub}(ec2,ec3)) ≤_{t} I_{sub}(ec1, ec3)
where ≤_{t} denotes the truth order on TV (see Section Model Theory for Condition Language of RIF BLD) and min_{t} is the minimum with respect to that truth order.
I_{isa} gives meaning to class membership. It is a truth-valued function D × D → TV. The truth valuation for classification formulas of the form o # cl, where o and cl are terms, is defined as follows:
I_{Truth}(o # cl) = I_{isa}(I(o), I(cl))
We also want # and ## to have the usual property that all members of a subclass are also members of the superclass, i.e., we want o # cl and cl ## scl to imply o # scl. To this end, we introduce the following restriction on the mappings I_{isa} and I_{sub}:
For all elements eo, ec, es ∈ D, the following must hold: min_{t}(I_{isa}(eo, ec), I_{sub}(ec,es)) ≤_{t} I_{isa}(eo, es)
where ≤_{t} and min_{t} are as before.
This section develops a RIF-BLD Rule Sublanguage by extending the RIF Condition Language, where conditions become rule bodies. RIF Phase I covers only Horn Rules and a number of extensions that do not increase the expressive power of the language. The envisioned RIF dialects will extend the RIF-BLD rule language by generalizing the positive RIF conditions and by other means.
This section defines Horn rules for RIF Phase 1. The syntax and semantics incorporates RIF Positive Conditions defined in Section Positive Conditions.
A rule is a statement of the form conclusion :- condition, where conclusion is a non-builtin atomic well-formed formula (i.e., formula with signature atomic but not bi_atomic); condition is a well-formed condition formula as defined in Sections Symbols and Signatures and Slotted Terms and Frames. All free variables in a rule are explicitly universally quantified outside of the rule. RIF also allows explicit existential quantification in the condition of the rules (for variables that occure only in the condition), but this is known to be equivalent to universal quantification outside of the rule due to the tautology (Forall ?X conclusion :- condition) ≡ (conclusion :- Exists ?X condition), if ?X occurs in condition only.
The overall structure of the syntax used in the RIF-BLD Horn rule sublanguage can be depicted using the following diagram, which extends the diagram shown in Section Positive Conditions.
The class Ruleset contains zero or more RULEs, where each RULE is one of the following classes:
Implies, which distinguishes if-CONDITION from then-ATOMIC parts (where ATOMIC represents the conclusion of the rule)
ATOMIC, which represents facts
Forall, which is specified through its parts, i.e. one or more variable (Var) declarations and, recursively, a RULE as the formula in their scope
Although not reflected in the diagram above or the EBNF syntax below, RIF requires explicit quantification of all variables. Therefore, variables that are not explicitly quantified in CONDITION must explicitly appear under a Forall.
The syntactic classes Var, CONDITION, and ATOMIC were specified in Section Positive Conditions.
The presentation syntax for Horn rules extends the syntax for Positive Conditions with the following productions.
EBNF grammar Ruleset ::= RULE* RULE ::= ' Forall ' Var+ ' ( ' RULE ' ) ' | Implies | ATOMIC Implies ::= ATOMIC ' :- ' CONDITION
Var, ATOMIC, and CONDITION were defined as part of the syntax for positive conditions in Positive Conditions. The symbol :- denotes the implication connective used in rules. The statement ATOMIC :- CONDITION should be informally read as if the premise CONDITION is true then the conclusion ATOMIC is also true. RIF deliberately avoids using the connective ← here because in some RIF dialects, such as LP and PR, the implication :- will have different meaning from the meaning of the first-order implication ←.
Rules are generated by the Implies production. Facts are generated by the ATOMIC production, and can be viewed as the then part of an Implies with an empty conjunctive if (or with true as the if part). The RULE production generates a rule or fact, possibly universally closed.
Note that, by definition, atomic formulas that correspond to builtin predicates (i.e., formulas with signature bi_atomic) are not allowed in the rule conclusions. This restriction is not reflected in the diagram or EBNF syntax above.
A ruleset is a set of RIF rules; it is generated by the production Ruleset.
Note also that, since CONDITION permits disjunction and existential quantification, the rules defined by the Implies production are more general than pure Horn rules. This extension was explained in the introduction to Section Positive Conditions.
Well-formed rules. A rule is well-formed iff its ATOMIC part is a well-formed atomic formula and the CONDITION part is a well-formed condition formula.
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 5 (A RIF rule in the presentation syntax) Here we use the prefix ppl as an abbreviation for http://example.com/people#. The prefix op is used for a yet-to-be-determined IRI, which will be used for RIF builtin predicates. a. Universal form: Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays ( reject^^rif:local ( ppl:John^^rif:iri ?item ) :- And ( perishable^^rif:local ( ?item ) delivered^^rif:local ( ?item ?deliverydate ppl:John^^rif:iri ) scheduled^^rif:local ( ?item ?scheduledate ) fn:subtract-dateTimes-yielding-dayTimeDuration ( ?deliverydate ?scheduledate ?diffuration ) fn:get-days-from-dayTimeDuration ( ?diffduration ?diffdays ) op:numeric-greater-than ( ?diffdays 10 ) ) ) b. Universal-existential form: Forall ?item ( reject^^rif:local ( ppl#John^^rif:iri ?item ) :- Exists ?deliverydate ?scheduledate ?diffduration ?diffdays ( And ( perishable^^rif:local ( ?item ) delivered^^rif:local ( ?item ?deliverydate ppl:John^^rif:iri ) scheduled^^rif:local ( ?item ?scheduledate ) fn:subtract-dateTimes-yielding-dayTimeDuration ( ?deliverydate ?scheduledate ?diffuration ) fn:get-days-from-dayTimeDuration ( ?diffduration ?diffdays ) op:numeric-greater-than ( ?diffdays 10 ) ) ) )
In form (a), all variables are quantified universally outside of the rule. In form (b), the variables that do not appear in the rule then part are instead quantified existentially in the if part. These two forms are logically equivalent.
The following extends the XML syntax of Positive Conditions, by serializing the above EBNF Syntax of RIF Horn rules in XML. The Forall element contains the role elements declare and formula, which were earlier used within the Exists element of Positive Conditions. 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 ATOMIC)
For the XML Schema Definition (XSD) of the RIF-BLD Horn rule language see Appendix Specification.
For instance, the rule in Example 5a can be serialized in XML as shown below as the first element of a rule set whose second element is a business rule for Fred.
Example 6 (A RIF rule set in XML syntax) <Ruleset> <rule> <Forall> <declare><Var>item</Var></declare> <declare><Var>deliverydate</Var></declare> <declare><Var>scheduledate</Var></declare> <declare><Var>diffduration</Var></declare> <declare><Var>diffdays</Var></declare> <formula> <Implies> <if> <And> <formula> <Uniterm> <op><Const type="rif:local">perishable</Const></op> <arg><Var>item</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">delivered</Const></op> <arg><Var>item</Var></arg> <arg><Var>deliverydate</Var></arg> <arg><Const type="rif:iri">ppl:John</Const></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">scheduled</Const></op> <arg><Var>item</Var></arg> <arg><Var>scheduledate</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">fn:subtract-dateTimes-yielding-dayTimeDuration</Const></op> <arg><Var>deliverydate</Var></arg> <arg><Var>scheduledate</Var></arg> <arg><Var>diffduration</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">fn:get-days-from-dayTimeDuration</Const></op> <arg><Var>diffduration</Var></arg> <arg><Var>diffdays</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:iri">op:numeric-greater-than</Const></op> <arg><Var>diffdays</Var></arg> <arg><Const type="xsd:long">10</Const></arg> </Uniterm> </formula> </And> </if> <then> <Uniterm> <op><Const type="xsd:long">reject</Const></op> <arg><Const type="rif:iri">ppl:John</Const></arg> <arg><Var>item</Var></arg> </Uniterm> </then> </Implies> </formula> </Forall> </rule> <rule> <Forall> <declare><Var>item</Var></declare> <formula> <Implies> <if> <Uniterm> <op><Const type="rif:local">unsolicited</Const></op> <arg><Var>item</Var></arg> </Uniterm> </if> <then> <Uniterm> <op><Const type="rif:local">reject</Const></op> <arg><Const type="rif:iri">ppl:Fred</Const></arg> <arg><Var>item</Var></arg> </Uniterm> </then> </Implies> </formula> </Forall> </rule> </Ruleset>
The translation between the presentation syntax and the XML syntax is given by a table that extends the translation tables of Positive Conditions and Slotted Conditions 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> |
Section Positive Conditions defined the notion of semantic structures and how such structures determine truth values of RIF conditions. The current section defines what it means for such a structure to satisfy a rule.
While semantic structures can be multivalued in RIF dialects that extend the BLD, rules are typically two-valued even in dialects that support inconsistency and uncertainty. Consider a rule of the form Q then :- if, where Q is a quantification prefix for all the variables in the rule. For the Horn subset, Q is a universal prefix, i.e., all variables in the rule are universally quantified outside of the rule. We first define the notion of rule satisfaction without the quantification prefix Q:
I |= then :- if |
iff I_{Truth}(then) ≥_{t} I_{Truth}(if). (Recall that the set of truth values, TV, has a partial order ≥_{t}.)
We define I |= Q then :- if iff I* |= then :- if for every I* that agrees with I everywhere except possibly on some variables mentioned in Q. In this case we also say that I is a model of the rule. I is a model of a rule set R, denoted I |= R, iff it is a model of every rule in the set, i.e., iff it is a semantic structure such that I |= r for every rule r ∈ R.
The above defines the semantics of RIF BLD using standard first-order semantics for Horn clauses. Various RIF dialects will extend this semantics in the required directions. Some of these extended semantics might not have a model theory (for example, production rules) and some will have non-first-order semantics. However, all these extensions are required to be compatible with the above definition when the rule set is completely covered by RIF BLD. This means that the set of intended models of such a rule set with respect to the extending dialect must coincide with the intended models defined by RIF BLD. For further details on defining the semantics for RIF dialects see end note on intended models for rule sets.
We will now define what it means for a set of rules to entail a RIF condition. Let S be a RIF ruleset and φ a closed RIF condition (a condition with no occurrences of free variables). Then we say that S entails φ, written as
S |= φ |
iff for every semantic structure I, such that I |= S, it is the case that I_{truth}(φ)=t.
Resource Description Framework (RDF): Concepts and Abstract Syntax, Klyne G., Carroll J. (Editors), W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/. Latest version available at http://www.w3.org/TR/rdf-concepts/.
RDF Semantics, Patrick Hayes, Editor, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-mt-20040210/. Latest version available at http://www.w3.org/TR/rdf-mt/.
RFC 3066 - Tags for the Identification of Languages, H. Alvestrand, IETF, January 2001. This document is http://www.isi.edu/in-notes/rfc3066.txt.
XML Schema Part 2: Datatypes, W3C Recommendation, World Wide Web Consortium, 2 May 2001. This version is http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/. The latest version is available at http://www.w3.org/TR/xmlschema-2/.
Normal Form Conventions for XML Representations of Structured Data, Henry S. Thompson. October 2001, As submitted to and accepted by XML 2001: For unclear reasons not published in their proceedings.
Logical foundations of object-oriented and frame-based languages, M. Kifer, G. Lausen, J. Wu. Journal of ACM, July 1995, pp. 741--843.
HiLog: A Foundation for higher-order logic programming, W. Chen, M. Kifer, D.S. Warren. Journal of Logic Programming, vol. 15, no. 3, February 1993, pp. 187--230.
Sorted HiLog: Sorts in Higher-Order Logic Data Languages, W. Chen, M. Kifer. Sixth Intl. Conference on Database Theory, Prague, Czech Republic, January 1995, Lecture Notes in Computer Science 893, Springer Verlag, pp. 252--265.
RDF/XML Syntax Specification (Revised), Dave Beckett, Editor, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-syntax-grammar-20040210/. Latest version available at http://www.w3.org/TR/rdf-syntax-grammar/.
The namespace of RIF is http://www.w3.org/2007/rif#.
XML schemas for the RIF BLD sublanguages are available below and online, which already helped to find and fix invalid parts in the examples.
<?xml version="1.0" encoding="UTF-8"?> <xs:schema xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns="http://www.w3.org/2007/rif#" targetNamespace="http://www.w3.org/2007/rif#" elementFormDefault="qualified" version="Id: RIFPosCond.xsd,v 0.6 2007/10/24 dhirtle"> <xs:annotation> <xs:documentation> This is a preliminary XML schema for Positive Conditions as defined by Working Draft 1 of the RIF Basic Logic Dialect. The schema is based on the following EBNF for the presentation syntax: CONDITION ::= 'And' ' ( ' CONDITION* ' ) ' | 'Or' ' ( ' CONDITION* ' ) ' | 'Exists' Var+ ' ( ' CONDITION ' ) ' | ATOMIC ATOMIC ::= Uniterm | Equal Uniterm ::= Const ' ( ' TERM* ' ) ' Equal ::= TERM ' = ' TERM TERM ::= Const | Var | Uniterm Const ::= LITERAL '^^' SYMSPACE Var ::= '?' VARNAME </xs:documentation> </xs:annotation> <xs:group name="CONDITION"> <!-- CONDITION ::= 'And' ' ( ' CONDITION* ' ) ' | 'Or' ' ( ' CONDITION* ' ) ' | 'Exists' Var+ ' ( ' CONDITION ' ) ' | ATOMIC --> <xs:choice> <xs:element ref="And"/> <xs:element ref="Or"/> <xs:element ref="Exists"/> <xs:group ref="ATOMIC"/> </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="ATOMIC"> <!-- ATOMIC ::= Uniterm | Equal --> <xs:choice> <xs:element ref="Uniterm"/> <xs:element ref="Equal"/> </xs:choice> </xs:group> <xs:element name="Uniterm"> <!-- Uniterm ::= Const ' ( ' TERM* ' ) ' --> <xs:complexType> <xs:sequence> <xs:element ref="op"/> <xs:element ref="arg" minOccurs="0" maxOccurs="unbounded"/> </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="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:group name="TERM"> <!-- TERM ::= Const | Var | Uniterm --> <xs:choice> <xs:element ref="Const"/> <xs:element ref="Var"/> <xs:element ref="Uniterm"/> </xs:choice> </xs:group> <xs:element name="Const"> <!-- Const ::= LITERAL '^^' SYMSPACE --> <xs:complexType mixed="true"> <xs:sequence/> <xs:attribute name="type" type="xs:string" use="required"/> </xs:complexType> </xs:element> <xs:element name="Var" type="xs:string"> <!-- Var ::= '?' VARNAME --> </xs:element> </xs:schema>
<?xml version="1.0" encoding="UTF-8"?> <xs:schema xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns="http://www.w3.org/2007/rif#" targetNamespace="http://www.w3.org/2007/rif#" elementFormDefault="qualified" version="Id: RIFSlotCond.xsd,v 0.6 2007/10/24 dhirtle"> <xs:annotation> <xs:documentation> This is a preliminary XML schema for Slotted Conditions as defined by Working Draft 1 of the RIF Basic Logic Dialect. The schema is based on the following EBNF for the presentation syntax: CONDITION ::= 'And' ' ( ' CONDITION* ' ) ' | 'Or' ' ( ' CONDITION* ' ) ' | 'Exists' Var+ ' ( ' CONDITION ' ) ' | ATOMIC ATOMIC ::= Uniterm | Equal | CLASSIFICATION | Frame Uniterm ::= Const ' ( ' (TERM* | (Const ' -> ' TERM)*) ' ) ' Equal ::= TERM '=' TERM CLASSIFICATION ::= TERM ' # ' TERM | TERM ' ## ' TERM Frame ::= (TERM | CLASSIFICATION) ' [ ' (TERM ' -> ' (TERM | Frame))* ' ] ' TERM ::= Const | Var | Uniterm Const ::= LITERAL '^^' SYMSPACE Var ::= '?' VARNAME </xs:documentation> </xs:annotation> <xs:group name="CONDITION"> <!-- CONDITION ::= 'And' ' ( ' CONDITION* ' ) ' | 'Or' ' ( ' CONDITION* ' ) ' | 'Exists' Var+ ' ( ' CONDITION ' ) ' | ATOMIC --> <xs:choice> <xs:element ref="And"/> <xs:element ref="Or"/> <xs:element ref="Exists"/> <xs:group ref="ATOMIC"/> </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="ATOMIC"> <!-- ATOMIC ::= Uniterm | Equal | CLASSIFICATION | Frame --> <xs:choice> <xs:element ref="Uniterm"/> <xs:element ref="Equal"/> <xs:group ref="CLASSIFICATION"/> <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:group name="CLASSIFICATION"> <!-- CLASSIFICATION ::= TERM ' # ' TERM | TERM ' ## ' TERM --> <xs:choice> <xs:element ref="Member"/> <xs:element ref="Subclass"/> </xs:choice> </xs:group> <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"> <!-- Frame ::= (TERM | CLASSIFICATION) ' [ ' (TERM ' -> ' (TERM | Frame))* ' ] ' --> <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:choice> <xs:group ref="TERM"/> <xs:element ref="Frame"/> </xs:choice> </xs:sequence> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="object"> <xs:complexType> <xs:choice> <xs:group ref="TERM"/> <xs:group ref="CLASSIFICATION"/> </xs:choice> </xs:complexType> </xs:element> <xs:group name="TERM"> <!-- TERM ::= Const | Var | Uniterm --> <xs:choice> <xs:element ref="Const"/> <xs:element ref="Var"/> <xs:element ref="Uniterm"/> </xs:choice> </xs:group> <xs:element name="Const"> <!-- Const ::= LITERAL '^^' SYMSPACE --> <xs:complexType mixed="true"> <xs:sequence/> <xs:attribute name="type" type="xs:string" use="required"/> </xs:complexType> </xs:element> <xs:element name="Var" type="xs:string"> <!-- Var ::= '?' VARNAME --> </xs:element> </xs:schema>
<?xml version="1.0" encoding="UTF-8"?> <xs:schema xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns="http://www.w3.org/2007/rif#" targetNamespace="http://www.w3.org/2007/rif#" elementFormDefault="qualified" version="Id: RIFPosHorn.xsd,v 0.6 2007/10/24 dhirtle"> <xs:annotation> <xs:documentation> This is a preliminary XML schema for Horn rules as defined by Working Draft 1 of the RIF Basic Logic Dialect. The schema is based on the following EBNF for the presentation syntax: Document ::= Ruleset* Ruleset ::= RULE* RULE ::= ' Forall ' Var+ ' ( ' RULE ' ) ' | Implies | ATOMIC Implies ::= ATOMIC ' :- ' CONDITION Note that this is an extension of the syntax for Positive Conditions. </xs:documentation> </xs:annotation> <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 name="rule" minOccurs="0" maxOccurs="unbounded"> <xs:complexType> <xs:group ref="RULE"/> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="RULE"> <!-- RULE ::= ' Forall ' Var+ ' ( ' RULE ' ) ' | Implies | ATOMIC --> <xs:choice> <xs:element ref="Forall"/> <xs:element ref="Implies"/> <xs:group ref="ATOMIC"/> </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="RULE"/> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Implies"> <!-- Implies ::= ATOMIC ' :- ' 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="ATOMIC"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="CONDITION"> <!-- CONDITION ::= 'And' ' ( ' CONDITION* ' ) ' | 'Or' ' ( ' CONDITION* ' ) ' | 'Exists' Var+ ' ( ' CONDITION ' ) ' | ATOMIC --> <xs:choice> <xs:element ref="And"/> <xs:element ref="Or"/> <xs:element ref="Exists"/> <xs:group ref="ATOMIC"/> </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> <!-- default formula; note different versions for Ruleset and Forall --> <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="ATOMIC"> <!-- ATOMIC ::= Uniterm | Equal --> <xs:choice> <xs:element ref="Uniterm"/> <xs:element ref="Equal"/> </xs:choice> </xs:group> <xs:element name="Uniterm"> <!-- Uniterm ::= Const ' ( ' TERM* ' ) ' --> <xs:complexType> <xs:sequence> <xs:element ref="op"/> <xs:element ref="arg" minOccurs="0" maxOccurs="unbounded"/> </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="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:group name="TERM"> <!-- TERM ::= Const | Var | Uniterm --> <xs:choice> <xs:element ref="Const"/> <xs:element ref="Var"/> <xs:element ref="Uniterm"/> </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>
Rationale: There are several equivalent ways to define first-order semantic structures. The one we adopted has the advantage that it generalizes to rule sets with negation as failure (NAF) and to logics for dealing with uncertainty and inconsistency. The difficulty is that some popular theories for NAF, such as the well-founded semantics, are based on three-valued semantic structures. Some popular ways to handle uncertain or inconsistent information (which is certainly important in the Web environment) rely on four-valued and other multi-valued logics. Therefore, following M. Fitting, Fixpoint Semantics for Logic Programming A Survey, Theoretical Computer Science, 1999, we build our definitions to be compatible with future RIF dialects, which will be based on multivalued logics.
Truth values: Some RIF dialects will have additional truth values. For instance, some versions of NAF use three truth values: t, f, and u (undefined). Handling of contradictions and uncertainty requires at least four truth values: t, u, f, and i (inconsistent).
Ordering truth values: In the well-founded semantics for NAF, f <_{t} u <_{t} t, and it is again a total order. But in four-valued logics, which are often used for dealing with uncertain or inconsistent information, the truth order is partial: f <_{t} u <_{t} t and f <_{t} i <_{t} t. Such logics also have another partial order, called the knowledge order <_{k}: u <_{k} t <_{k} i; and u <_{k} f <_{k} i. Under the knowledge order, true and false are incomparable, and facts that are both true and false receive the truth value i, which is the least upper bound of f and t in the knowledge order.
Intended models for rule sets: The notion of a model is only the basic ingredient in the definition of a semantics of a rule set. In general, a semantics of a rule set R is the set of its intended models (see Y. Shoham. Nonmonotonic logics: meaning and utility. In: Proc. 10th International Joint Conference on Artificial Intelligence, Morgan Kaufmann, pp. 388--393, 1987). There are different theories of what the intended sets of models are supposed to look like depending on the features of the particular rule sets.
For the basic logic dialect, which is based on Horn rules, the set of intended models of R is commonly agreed upon: it is the unique minimal model of R.
However, when rule bodies contain literals negated with the negation-as-failure connective naf, then only some of the minimal models of a rule set are viewed as intended. This issue will be addressed in the appropriate dialects of RIF. The two most common theories of intended models are based on the so called well-founded models and stable models. Here we will just illustrate the problem with a simple example.
Suppose R consists of a single rule p :- naf q. If naf were interpreted as classical negation, not, then this rule would be simply equivalent to p \/ q, and so it would have two kinds of models: one in which p is true and one where q is true. In contrast to first-order logic, most rule-based systems do not consider p and q symmetrically. Instead, they view the rule p :- naf q as a statement that p must be true if it is not possible to establish the truth of q. Since it is, indeed, impossible to establish the truth of q, such theories will derive p even though it does not logically follow from p \/ q. The logic underlying rule-based systems also assumes that only the minimal models are intended (minimality here is with respect to the set of true facts). Therefore, the intended models of the above rule set R must have the property that not only p is true but also that q is false.