Copyright © 2008 W3C® (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark and document use rules apply.
This document, developed by the Rule Interchange Format (RIF) Working Group, specifies a basic format that allows logic rules to be exchanged between rule-based systems.
A separate document RIF Data Types and Built-Ins describes data types and built-in functions and predicates.
This section describes the status of this document at the time of its publication. Other documents may supersede this document. A list of current W3C publications and the latest revision of this technical report can be found in the W3C technical reports index at http://www.w3.org/TR/.
This document is being published as one of a set of 6 documents:
The Rule Interchange Format (RIF) Working Group seeks public feedback on these Working Drafts. Please send your comments to public-rif-comments@w3.org (public archive). If possible, please offer specific changes to the text that would address your concern. You may also wish to check the Wiki Version of this document for internal-review comments and changes being drafted which may address your concerns.
Publication as a Working Draft does not imply endorsement by the W3C Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress.
This document was produced by a group operating under the 5 February 2004 W3C Patent Policy. W3C maintains a public list of any patent disclosures made in connection with the deliverables of the group; that page also includes instructions for disclosing a patent. An individual who has actual knowledge of a patent which the individual believes contains Essential Claim(s) must disclose the information in accordance with section 6 of the W3C Patent Policy.
Contents |
This document develops RIF-BLD (the Basic Logic Dialect of the Rule Interchange Format). 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 as in F-logic [KLW95], internationalized resource identifiers (or IRIs, defined by [RFC-3987]) as identifiers for concepts, and XML Schema data types. In addition, the document RIF RDF and OWL Compatibility defines the syntax and semantics of integrated RIF-BLD/RDF and RIF-BLD/OWL languages. These features make RIF-BLD a Web-aware language. However, it should be kept in mind that RIF is designed to enable interoperability among rule languages in general, and its uses are not limited to the Web.
RIF-BLD is defined in two different ways -- both normative:
This version of the RIF-BLD specification is very short and is presented at the end of this document, in Section RIF-BLD as a Specialization of the RIF Framework. It is intended for the reader who is familiar with RIF-FLD and, therefore, does not need to go through the much longer direct specification of RIF-BLD. This version of the specification is also useful for dialect designers, as it is a concrete example of how a non-trivial RIF dialect can be derived from the RIF framework for logic dialects.
Logic-based RIF dialects that extend RIF-BLD in accordance with the RIF Framework for Logic Dialects will be specified in other documents by this working group.
This normative section specifies the syntax of RIF-BLD directly, without relying on RIF-FLD. We define both the presentation syntax and an XML syntax. The presentation syntax is normative, but not intended to be a concrete syntax for RIF-BLD. It is defined in mathematical English and is meant to be used in the definitions and examples. This syntax deliberately leaves out details such as the delimiters of the various syntactic components, escape symbols, parenthesizing, precedence of operators, and the like. Since RIF is an interchange format, it uses XML as its concrete syntax.
Note to the reader: this section depends on Section Constants, Symbol Spaces, and Data Types of the document Data Types and Builtins.
Definition (Alphabet). The alphabet of the presentation language of RIF-BLD consists of
The set of connective symbols, quantifiers, =, etc., is disjoint from Const and Var. The argument names in ArgNames are written as unicode strings that must not start with a question mark, "?". Variables are written as Unicode strings preceded with the symbol "?".
Constants are written as "literal"^^symspace, where literal is a sequence of Unicode characters and symspace is an identifier for a symbol space. Symbol spaces are defined in Section Constants and Symbol Spaces of the document Data Types and Builtins.
The symbols =, #, and ## are used in
formulas that define equality, class membership, and subclass
relationships. The symbol -> is used in terms that have
named arguments and in frame formulas. The symbol External
indicates that an atomic formula or a function term is defined
externally (e.g., a builtin) and the symbols Prefix and
Base are used in abridged representations of IRIs.
The symbol Document is used to define RIF-BLD documents, Import is an import directive, and the symbol Group is used to organize RIF-BLD formulas into collections. ☐
The language of RIF-BLD is the set of formulas constructed using the above alphabet according to the rules given below.
RIF-BLD defines several kinds of terms: constants and variables, positional terms, terms with named arguments, plus equality, membership, subclass, frame, and external terms. The word "term" will be used to refer to any of these constructs.
To simplify the language in the next definition, we will use the following terminology:
t is a positional or a named-argument term.
Definition (Term).
The constant t here represents a predicate or a function; s1, ..., sn represent argument names; and v1, ..., vn represent argument values. The argument names, s1, ..., sn, are required to be pairwise distinct. Terms with named arguments are like positional terms except that the arguments are named and their order is immaterial. Note that a term of the form f() is both positional and with named arguments.
Membership, subclass, and frame terms are used to describe objects and class hierarchies.
Such terms are used for representing builtin functions and predicates as well as "procedurally attached" terms or predicates, which might exist in various rule-based systems, but are not specified by RIF. ☐
Note that frame terms are allowed to be externally defined. Therefore, externally defined objects can be accessed using the more natural frame-based interface. For instance, External("http://example.com/acme"^^rif:iri["http://example.com/acme/president"^^rif:iri(?Year) -> ?Pres]) could be an interface provided to access an externally defined method "http://example.com/mycompany/president"^^rif:iri in an external object "http://example.com/acme"^^rif:iri.
The set of all symbols, Const, is partitioned into
The symbols in Const that belong to the supported RIF data types are individuals.
Each predicate and function symbol has precisely one arity.
The arity of a symbol (or whether it is a predicate, a function, or an individual) is not specified in RIF-BLD explicitly. Instead, it is inferred as follows. Each constant symbol, p, in a RIF-BLD formula (or a set of formulas) may occur in at most one context:
This means that p is a term by itself, which appears inside some other term (positional, with named arguments, in a frame, etc.).
This means that p occurs in a term t of the form p(...) and t itself occurs inside some other term.
This means that p occurs in a term t of the form p(...) and t does not occur inside some other term.
The arity of the symbol and its type is determined by its context. If a symbol from Const occurs in more than one context in a set of formulas, the set is not well-formed in RIF-BLD.
For a term of the form External(t) to be well-formed, t must be an instance of an external schema, i.e., a schema of an externally specified term, as defined in Section Schemas for Externally Defined Terms of the document Data Types and Builtins.
Also, if a term of the form External(p(...)) occurs as an atomic formula then p is considered a predicate symbol.
A well-formed
term is one that occurs in a well-formed set of
fomulas.
Any term (positional or with named arguments) of the form p(...), where p is a predicate symbol, is also an atomic formula. Equality, membership, subclass, and frame terms are also atomic formulas. A statement of the form External(φ), where φ is an atomic formula, is also an atomic formula, called an externally defined atomic formula.
Simple terms (constants and variables) are not formulas. Not all atomic formulas are well-formed. A well-formed atomic formula is an atomic formula that is also a well-formed term (see Section Well-formedness of Terms). More general formulas are constructed out of the atomic formulas with the help of logical connectives.
Definition (Well-formed formula). A well-formed formula is a statement that has one of the following forms:
Condition formulas are intended to be used inside the premises of rules. Next we define the notion of a RIF-BLD rule, sets of rules, and RIF documents.
Group formulas are used to represent sets of rules. Note that some of the ρi's can be group formulas themselves, which means that groups can be nested.
Section Direct Specification of RIF-BLD Semantics of this document defines the semantics for the directive Import(t) only. The semantics of the directive Import(t p) is given in the document RIF RDF and OWL Compatibility. It is used for importing non-RIF-BLD logical entities, such as RDF data and OWL ontologies. The profile specifies what kind of entity is being imported and under what semantics (for instance, the various RDF entailment regimes).
Prefix directives do not affect the semantics of RIF documents. Instead, they are used as shorthands to allow more concise representation of IRI constants. This mechanism is explained in the document Data Types and Builtins, Section Constants and Symbol Spaces.
Like prefix directives, base directives do not affect the semantics. They are used as syntactic shortcuts for expanding relative IRIs into full IRIs, as described in Section Constants and Symbol Spaces of the document Data Types and Builtins.
The above definitions endow RIF-BLD with a wide variety of
syntactic forms for terms and formulas, which creates
infrastructure for exchanging syntactically diverse rule languages.
Systems that do not support some of the syntax directly can still
support it through syntactic transformations. For instance,
disjunctions in the rule body can be eliminated through a standard
transformation, such as replacing p :- Or(q r) with a
pair of rules p :- q, p :- r. Terms with
named arguments can be reduced to positional terms by ordering the
arguments by their names and incorporating them into the predicate
name. For instance, p(bb->1 aa->2) can be
represented as p_aa_bb(2,1).
RIF-BLD allows every term to be optionally preceded by a metadata block of the form (* id φ *) where id is a rif:iri constant and φ is a frame formula or a conjunction of frame formulas. Both items inside the metadata block are optional. The id part represents the meta-identifier of the term to which the metadata block is attached and φ is the metadata itself. RIF-BLD does not impose any restrictions on φ apart from what is stated above. In particular, it may include variables, function symbols, rif:local constants, and so on.
Observe that there is certain syntactic ambiguity in the above definition. For instance, in (* id φ *) t[w -> v] the metadata block can be attributed to the term t or to the entire frame t[w -> v]. We do not make an attempt to resolve this ambiguity in the presentation syntax, since, as explained earlier, this syntax is not intended to be concrete. The concrete XML syntax of RIF-BLD does not have such ambiguities.
It is suggested to use Dublin Core, RDFS, and OWL properties for metadata, along the lines of http://www.w3.org/TR/owl-ref/#Annotations -- specifically owl:versionInfo, rdfs:label, rdfs:comment, rdfs:seeAlso, rdfs:isDefinedBy, dc:creator, dc:description, dc:date, and foaf:maker.
So far, the syntax of RIF-BLD has been specified in mathematical English. Tool developers, however, may prefer EBNF notation, which provides a more succinct overview of the syntax. Several points should be kept in mind regarding this notation.
The Condition Language represents formulas that can be used in the body of RIF-BLD rules. The EBNF grammar for a superset of the RIF-BLD condition language is as follows.
FORMULA ::= 'And' '(' FORMULA* ')' | 'Or' '(' FORMULA* ')' | 'Exists' Var+ '(' FORMULA ')' | ATOMIC | 'External' '(' Atom | Frame ')' ATOMIC ::= Atom | Equal | Member | Subclass | Frame Atom ::= UNITERM UNITERM ::= Const '(' (TERM* | (Name '->' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '->' TERM)* ']' TERM ::= Const | Var | Expr | 'External' '(' Expr ')' Expr ::= UNITERM Const ::= '"' UNICODESTRING '"^^' SYMSPACE Name ::= UNICODESTRING Var ::= '?' UNICODESTRING SYMSPACE ::= UNICODESTRING
The production rule for the non-terminal FORMULA
represents RIF condition formulas (defined earlier). The
connectives And and Or define conjunctions and
disjunctions of conditions, respectively. Exists
introduces existentially quantified variables. Here Var+
stands for the list of variables that are free in FORMULA.
RIF-BLD conditions permit only existential variables. A RIF-BLD
FORMULA can also be an ATOMIC term, i.e. an
Atom, External Atom, Equal,
Member, Subclass, or Frame. A
TERM can be a constant, variable, Expr, or
External Expr.
The RIF-BLD presentation syntax does not commit to any particular vocabulary and permits arbitrary Unicode strings in constant symbols, argument names, and variables. Constant symbols have the form: "UNICODESTRING"^^SYMSPACE, where SYMSPACE is a Unicode string that represents an identifier or an alias of the symbol space of the constant, and UNICODESTRING is a Unicode string from the lexical space of that symbol space. Names are denoted by Unicode character sequences. Variables are denoted by a UNICODESTRING prefixed with a ?-sign. Equality, membership, and subclass terms are self-explanatory. An Atom and Expr (expression) can either be positional or with named arguments. A frame term is a term composed of an object Id and a collection of attribute-value pairs. An External(Atom) is a call to an externally defined predicate; External(Frame) is a call to an externally defined frame. Likewise, External(Expr) is a call to an externally defined function.
Example 1 (RIF-BLD conditions).
This example shows conditions that are composed of atoms, expressions, frames, and existentials. In frame formulas variables are shown in the positions of object Ids, object properties, and property values. For brevity, we use the shortcut notation prefix:suffix, which should be understood as a macro that expands into an IRI obtained by concatenation of the prefix definition and suffix. Thus, if bks is a prefix that expands into http://example.com/books# then bks:LeRif is an abbreviation for "http://example.com/books#LeRif"^^rif:iri. This and other shortcuts are defined in the document Data Types and Builtins. Assume that the following prefix directives appear in the preamble to the document:
Prefix(bks http://example.com/books#) Prefix(auth http://example.com/authors#) Prefix(cpt http://example.com/concepts#)
Positional terms: cpt:book(auth:rifwg bks:LeRif) Exists ?X (cpt:book(?X bks:LeRif)) Terms with named arguments: cpt:book(cpt:author->auth:rifwg cpt:title->bks:LeRif) Exists ?X (cpt:book(cpt:author->?X cpt:title->bks:LeRif)) Frames: bks:wd1[cpt:author->auth:rifwg cpt:title->bks:LeRif] Exists ?X (bks:wd2[cpt:author->?X cpt:title->bks:LeRif]) Exists ?X (And (bks:wd2#cpt:book bks:wd2[cpt:author->?X cpt:title->bks:LeRif])) Exists ?I ?X (?I[cpt:author->?X cpt:title->bks:LeRif]) Exists ?I ?X (And (?I#cpt:book ?I[cpt:author->?X cpt:title->bks:LeRif])) Exists ?S (bks:wd2[cpt:author->auth:rifwg ?S->bks:LeRif]) Exists ?X ?S (bks:wd2[cpt:author->?X ?S->bks:LeRif]) Exists ?I ?X ?S (And (?I#cpt:book ?I[author->?X ?S->bks:LeRif]))
The presentation syntax for RIF-BLD rules extends the syntax in Section EBNF for RIF-BLD Condition Language with the following productions.
Document ::= IRIMETA? 'Document' '(' DIRECTIVE* Group? ')' DIRECTIVE ::= Import | Prefix | Base Import ::= 'Import' '(' IRI PROFILE? ')' Prefix ::= 'Prefix' '(' Name IRI ')' Base ::= 'Base' '(' IRI ')' Group ::= IRIMETA? 'Group' '(' (RULE | Group)* ')' RULE ::= IRIMETA? 'Forall' Var+ '(' CLAUSE ')' | CLAUSE CLAUSE ::= Implies | ATOMIC Implies ::= IRIMETA? ATOMIC ':-' FORMULA IRIMETA ::= '(*' Const? (Frame | 'And' '(' Frame* ')')? '*)' IRI ::= UNICODESTRING PROFILE ::= UNICODESTRING
For convenient reference, we reproduce the condition language part of the EBNF below.
FORMULA ::= 'And' '(' FORMULA* ')' | 'Or' '(' FORMULA* ')' | 'Exists' Var+ '(' FORMULA ')' | ATOMIC | 'External' '(' ATOMIC ')' ATOMIC ::= Atom | Equal | Member | Subclass | Frame Atom ::= UNITERM UNITERM ::= Const '(' (TERM* | (Name '->' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '->' TERM)* ']' TERM ::= Const | Var | Expr | 'External' '(' Expr ')' Expr ::= UNITERM Const ::= '"' UNICODESTRING '"^^' SYMSPACE Name ::= UNICODESTRING Var ::= '?' UNICODESTRING SYMSPACE ::= UNICODESTRING
A RIF-BLD Document, Group, etc. can be prefixed with optional identifier-metadata annotations, IRIMETA. IRIMETA is represented using (*...*)-brackets that contain an optional Const as identifier followed by an optional Frame or conjunction of Frames as metadata. A RIF-BLD Document consists of an optional DIRECTIVE preamble and an optional Group main part. A DIRECTIVE can be any number of Imports, Prefixes, or Bases. A RIF-BLD Group is a nested collection of any number of RULEs along with any number of nested Groups. Rules are generated by CLAUSE, which can be in the scope of a Forall quantifier. If a CLAUSE in the RULE production has a free (non-quantified) variable, it must occur in the Var+ sequence. Frame, Var, ATOMIC, and FORMULA were defined as part of the syntax for positive conditions in Section EBNF for RIF-BLD Condition Language. In the CLAUSE production an ATOMIC is treated as a rule with an empty condition part -- in which case it is usually called a fact. Note that, by a definition in Section Formulas, formulas that query externally defined atoms (i.e., formulas of the form External(Atom(...))) are not allowed in the conclusion part of a rule (ATOMIC does not expand to External).
Example 2 (RIF-BLD rules).
This example shows a business rule borrowed from the document RIF Use Cases and Requirements:
As before, for better readability we use the compact URI notation defined in [[DTB|Data Types and Builtins, Section Constants and Symbol Spaces. Again, prefix directives are assumed in the preamble to the document. Then, two versions of the main part of the document are given.
Prefix(ppl http://example.com/people#) Prefix(cpt http://example.com/concepts#) Prefix(op http://www.w3.org/2007/rif-builtin-predicate#) a. Universal form: Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays ( cpt:reject(ppl:John ?item) :- And(cpt:perishable(?item) cpt:delivered(?item ?deliverydate ppl:John) cpt:scheduled(?item ?scheduledate) External(fn:subtract-dateTimes-yielding-dayTimeDuration(?deliverydate ?scheduledate ?diffduration)) External(fn:get-days-from-dayTimeDuration(?diffduration ?diffdays)) External(op:numeric-greater-than(?diffdays 10))) ) b. Universal-existential form: Forall ?item ( cpt:reject(ppl:John ?item ) :- Exists ?deliverydate ?scheduledate ?diffduration ?diffdays ( And(cpt:perishable(?item) cpt:delivered(?item ?deliverydate ppl:John) cpt:scheduled(?item ?scheduledate) External(fn:subtract-dateTimes-yielding-dayTimeDuration(?deliverydate ?scheduledate ?diffduration)) External(fn:get-days-from-dayTimeDuration(?diffduration ?diffdays)) External(op:numeric-greater-than(?diffdays 10))) ) )
Example 3 (A RIF-BLD document containing a group annotated
with metadata).
This example shows a complete document containing a group formula that consists of two RIF-BLD rules. The first of these rules is copied from Example 2a. The group is annotated with an IRI identifier and frame-represented Dublin Core metadata.
Document( Prefix(ppl http://example.com/people#) Prefix(cpt http://example.com/concepts#) Prefix(dc http://purl.org/dc/terms/) Prefix(w3 http://www.w3.org/) Prefix(op http://www.w3.org/2007/rif-builtin-predicate#) Prefix(xsd http://www.w3.org/2001/XMLSchema#) (* <http://sample.org> pd[dc:publisher -> w3:W3C dc:date -> "2008-04-04"^^xsd:date] *) Group ( Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays ( cpt:reject(ppl:John ?item) :- And(cpt:perishable(?item) cpt:delivered(?item ?deliverydate ppl:John) cpt:scheduled(?item ?scheduledate) External(fn:subtract-dateTimes-yielding-dayTimeDuration(?deliverydate ?scheduledate ?diffduration)) External(fn:get-days-from-dayTimeDuration(?diffduration ?diffdays)) External(op:numeric-greater-than(?diffdays 10))) ) Forall ?item ( cpt:reject(ppl:Fred ?item) :- cpt:unsolicited(?item) ) ) )
This normative section specifies the semantics of RIF-BLD directly, without relying on RIF-FLD.
Recall that the presentation syntax of RIF-BLD allows the use of macros, which are specified via the Prefix and Base directives. The semantics, below, is described using the full syntax, i.e., the description assumes that all macros have already been expanded as explained in Data Types and Builtins, Section Constants and Symbol Spaces.
The set TV of truth values in RIF-BLD consists of just two values, t and f.
The key concept in a model-theoretic semantics of a logic language is the notion of a semantic structure. The definition, below, is a little bit more general than necessary. This is done in order to better see the connection with the semantics of the RIF framework.
Definition (Semantic structure). A semantic structure, I, is a tuple of the form <TV, DTS, D, Dind, Dfunc, IC, IV, IF, Iframe, ISF, Isub, Iisa, I=, Iexternal, Itruth>. Here D is a non-empty set of elements called the domain of I, and Dind, Dfunc are nonempty subsets of D. Dind is used to interpret the elements of Const, which denote individuals and Dfunc is used to interpret the elements of Const, which denote function symbols. As before, Const denotes the set of all constant symbols and Var the set of all variable symbols. TV denotes the set of truth values that the semantic structure uses and DTS is a set of identifiers for primitive data types (please refer to Section Data Types of the document Data Types and Builtins for the semantics of data types).
The other components of I are total mappings defined as follows:
This mapping interprets constant symbols. In addition:
This mapping interprets variable symbols.
This mapping interprets positional terms. In addition:
This mapping interprets function symbols with named arguments. In addition:
This mapping interprets frame terms. An argument, d ∈ Dind, to Iframe represent an object and the finite bag {<a1,v1>, ..., <ak,vk>} represents a bag of attribute-value pairs for d. We will see shortly how Iframe is used to determine the truth valuation of frame terms.
Bags (multi-sets) are used here because the order of the attribute/value pairs in a frame is immaterial and pairs may repeat: o[a->b a->b]. Such repetitions arise naturally when variables are instantiated with constants. For instance, o[?A->?B ?C->?D] becomes o[a->b a->b] if variables ?A and ?C are instantiated with the symbol a and ?B, ?D with b.
The operator ## is required to be transitive, i.e., c1 ## c2 and c2 ## c3 must imply c1 ## c3. This is ensured by a restriction in Section Interpretation of Formulas.
The relationships # and ## are required to have the usual property that all members of a subclass are also members of the superclass, i.e., o # cl and cl ## scl must imply o # scl. This is ensured by a restriction in Section Interpretation of Formulas.
It gives meaning to the equality operator.
It is used to define truth valuation for formulas.
For every external schema, σ, associated with the language, Iexternal(σ) is assumed to be specified externally in some document (hence the name external schema). In particular, if σ is a schema of a RIF builtin predicate or function, Iexternal(σ) is specified in the document Data Types and Builtins so that:
For convenience, we also define the following mapping I from terms to D:
Here we use {...} to denote a set of argument/value pairs.
Here {...} denotes a bag of attribute/value pairs.
Note that, by definition, External(t) is well formed only if t is an instance of an external schema. Furthermore, by the definition of coherent sets of external schemas, t can be an instance of at most one such schema, so I(External(t)) is well-defined.
The effect of data types. The data types in DTS impose the following restrictions. If dt ∈ DTS is a symbol space identifier of a data type, let LSdt denote the lexical space of dt, VSdt denote its value space, and Ldt: LSdt → VSdt the lexical-to-value-space mapping (for the definitions of these concepts, see Section Primitive Data Types of the document Data Types and Builtins). Then the following must hold:
That is, IC must map the constants of a data type dt in accordance with Ldt.
RIF-BLD does not impose restrictions on IC for constants in the lexical spaces that do not correspond to primitive datatypes in DTS. ☐
Observe that metadata blocks are ignored by all the mappings that constitue RIF-BLD semantic structures, so metadata has no effect on the formal semantics.
Note that although metadata associated with RIF-BLD formulas is ignored by the semantics, it can be extracted by XML tools. Since metadata is represented by frame terms, it can be reasoned with by RIF-BLD rules.
This section defines how a semantic structure, I, determines the truth value TValI(φ) of a RIF-BLD formula, φ, where φ is any formula other than a document formula. Truth valuation of document formulas is defined in the next section.
To this end, we define a mapping, TValI, from the set of all non-document formulas to TV. Note that the definition implies that TValI(φ) is defined only if the set DTS of the data types of I includes all the data types mentioned in φ.
Definition (Truth valuation). Truth valuation for well-formed formulas in RIF-BLD is determined using the following function, denoted TValI:
To ensure that the operator ## is transitive, i.e., c1 ## c2 and c2 ## c3 imply c1 ## c3, the following is required:
To ensure that all members of a subclass are also members of the superclass, i.e., o # cl and cl ## scl implies o # scl, the following is required:
Since the bag of attribute/value pairs represents the conjunctions of all the pairs, the following is required:
Note that, by definition, External(t) is well-formed only if t is an instance of an external schema. Furthermore, by the definition of coherent sets of external schemas, t can be an instance of at most one such schema, so I(External(t)) is well-defined.
The empty conjunction is treated as a tautology, so TValI(And()) = t.
The empty disjunction is treated as a contradiction, so TValI(Or()) = f.
Here I* is a semantic structure of the form <TV, DTS, D, Dind, Dfunc, IC, I*V, IF, Iframe, ISF, Isub, Iisa, I=, Iexternsl, Itruth>, which is exactly like I, except that the mapping I*V, is used instead of IV. I*V is defined to coincide with IV on all variables except, possibly, on ?v1,...,?vn.
If Γ is a group formula of the form Group(ρ1 ... ρn) then
This means that a group of rules is treated as a conjunction. ☐
Document formulas are interpreted using semantic multi-structures.
Definition (Semantic multi-structures). A semantic multi-structure is a set {IΔ1, ..., IΔn}, n>0, where IΔ1, ..., IΔn are semantic structures labeled with document formulas. These structures must be identical in all respects except that the mappings ICΔ1, ..., ICΔn might differ on the constants in Const that belong to the rif:local symbol space. The above set is allowed to have at most one semantic structure with the same label. ☐
Definition (Imported document). Let Δ be a document
formula and Import(t) be one of its import directives,
which references another document formula, Δ'. In this
case, we say that Δ' is directly imported
into Δ.
A document formula Δ' is said to be imported into Δ if it is either directly imported into Δ or it is imported (directly or not) into another formula, which is directly imported into Δ. ☐
With the help of semantic multi-structures we can now explain the semantics of RIF documents.
Definition (Truth valuation of document formulas). Let Δ be a document formula and let Δ1, ..., Δk be all the RIF-BLD document formulas that are imported (directly or indirectly, according to the previous definition) into Δ. Let Γ, Γ1, ..., Γk denote the respective group formulas associated with these documents. If any of these Γi is missing (which is a possibility, since every part of a document is optional), assume that it is a tautology, such as a = a, so that every TVal function maps such a Γi to the truth value t. Let I = {IΔ, IΔ1, ..., IΔk, ...} be a semantic multi-structure, which contains semantic structures labeled with at least the documents Δ, Δ1, ..., Δk. Then we define:
Note that this definition considers only those document formulas that are reachable via the one-argument import directives. Two argument import directives are ignored here. Their semantics is defined by the document RIF RDF and OWL Compatibility. ☐
The above definitions make the intent behind the rif:local
constants clear: rif:local constants that occur in
different documents can be interpreted differently even if they
have the same name. Therefore, each document can choose the names
for the rif:local constants freely and without regard to
the names of such constants used in the imported documents.
We now define what it means for a set of RIF-BLD rules (such as a group or a document formula) to entail a RIF-BLD condition. In this context, condition formulas play the role of queries to the RIF-BLD knowledge base and, therefore, entailment of condition formulas gives formal underpinning to RIF-BLD queries.
From now on, every formula is assumed to be part of some document.
If it is not physically part of any document, it will be said to
belong to a special query document. If I is a
semantic multi-structure, Δ is the document of φ,
and IΔ is a component structure
in I, then TValI(φ) is
defined as TValIΔ(φ).
Otherwise, TValI(φ) is undefined.
Definition (Models). A multi-structure I is a model of a formula, φ, written as I|=φ, iff TValI(φ) is defined and equals t. ☐
Definition (Logical entailment). Let Γ and φ be RIF-BLD formulas. We say that Γ entails φ, written as Γ |= φ, if and only if every multi-structure I that is a model of Γ is also a model of φ. ☐
Note that one consequence of the multi-document semantics of
RIF-BLD is that local constants specified in one document cannot be
queried from another document. In particular, they cannot be
returned as query answers. For instance, if one document,
Δ', has the fact
"http://example.com/ppp"^^rif:iri("abc"^^rif:local) while
another document formula, Δ, imports Δ' and has
the rule "http://example.com/qqq"^^rif:iri(?X) :-
"http://example.com/ppp"^^rif:iri(?X) , then Δ |=
"http://example.com/qqq"^^rif:iri("abc"^^rif:local) does
not hold. This is because "abc"^^rif:local in
Δ' and "abc"^^rif:local in the query on the
right-hand side of |= are treated as different constants
by semantic multi-structures.
RIF-BLD uses XML 1.0 (Fourth Edition) for its XML syntax.
The XML serialization for RIF-BLD is alternating or fully striped [ANF01]. A fully striped serialization views XML documents as objects and divides all XML tags into class descriptors, called type tags, and property descriptors, called role tags. We use capitalized names for type tags and lowercase names for role tags.
The all-uppercase classes in the presentation syntax, such as FORMULA, become XML Schema groups in Appendix XML Schema for BLD. 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.
XML serialization of RIF-BLD in Section EBNF for RIF-BLD Condition Language uses the following elements.
- And (conjunction) - Or (disjunction) - Exists (quantified formula for 'Exists', containing declare and formula roles) - declare (declare role, containing a Var) - formula (formula role, containing a FORMULA) - Atom (atom formula, positional or with named arguments) - External (external call, containing a content role) - content (content role, containing an Atom, for predicates, or Expr, for functions) - Member (member formula) - Subclass (subclass formula) - Frame (Frame formula) - object (Member/Frame role, containing a TERM or an object description) - op (Atom/Expr role for predicates/functions as operations) - args (Atom/Expr positional arguments role, containing n TERMs) - instance (Member instance role) - class (Member class role) - sub (Subclass sub-class role) - super (Subclass super-class role) - slot (Atom/Expr or Frame slot role, containing a Name or TERM followed by a TERM) - Equal (prefix version of term equation '=') - Expr (expression formula, positional or with named arguments) - side (Equal left-hand side and right-hand side role) - Const (individual, function, or predicate symbol, with optional 'type' attribute) - Name (name of named argument) - Var (logic variable)
For the XML Schema Definition (XSD) of the RIF-BLD condition language see Appendix XML Schema for BLD.
The XML syntax for symbol spaces utilizes the type attribute associated with XML term elements such as Const. For instance, a literal in the xsd:dateTime data type can be represented as <Const type="&xsd;dateTime">2007-11-23T03:55:44-02:30</Const>. RIF-BLD also utilizes the ordered attribute to indicate the orderedness of children of the elements args and slot it is associated with.
Example 4 (A RIF condition and its XML serialization).
This example illustrates XML serialization for RIF conditions. As before, the compact URI notation is used for better readability. Assume that the following prefix directives are found in the preamble to the document:
Prefix(bks http://example.com/books#) Prefix(cpt http://example.com/concepts#) Prefix(curr http://example.com/currencies#) Prefix(rif http://www.w3.org/2007/rif#) Prefix(xsd http://www.w3.org/2001/XMLSchema#)
RIF condition And (Exists ?Buyer (cpt:purchase(?Buyer ?Seller cpt:book(?Author bks:LeRif) curr:USD(49))) ?Seller=?Author ) XML serialization <And> <formula> <Exists> <declare><Var>Buyer</Var></declare> <formula> <Atom> <op><Const type="&rif;iri">&cpt;purchase</Const></op> <args rif:ordered="yes"> <Var>Buyer</Var> <Var>Seller</Var> <Expr> <op><Const type="&rif;iri">&cpt;book</Const></op> <args rif:ordered="yes"> <Var>Author</Var> <Const type="&rif;iri">&bks;LeRif</Const> </args> </Expr> <Expr> <op><Const type="&rif;iri">&curr;USD</Const></op> <args rif:ordered="yes"><Const type="&xsd;integer">49</Const></args> </Expr> </args> </Atom> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And>
Example 5 (A RIF condition with named arguments and its XML
serialization).
This example illustrates XML serialization of RIF conditions that involve terms with named arguments. As in Example 4, we assume the following prefix directives:
Prefix(bks http://example.com/books#) Prefix(cpt http://example.com/concepts#) Prefix(curr http://example.com/currencies#) Prefix(rif http://www.w3.org/2007/rif#) Prefix(xsd http://www.w3.org/2001/XMLSchema#)
RIF condition: And (Exists ?Buyer ?P ( And (?P#cpt:purchase ?P[cpt:buyer->?Buyer cpt:seller->?Seller cpt:item->cpt:book(cpt:author->?Author cpt:title->bks:LeRif) cpt:price->49 cpt:currency->curr:USD])) ?Seller=?Author) XML serialization: <And> <formula> <Exists> <declare><Var>Buyer</Var></declare> <declare><Var>P</Var></declare> <formula> <And> <formula> <Member> <instance><Var>P</Var></instance> <class><Const type="&rif;iri">&cpt;purchase</Const></class> </Member> </formula> <formula> <Frame> <object> <Var>P</Var> </object> <slot rif:ordered="yes"> <Const type="&rif;iri">&cpt;buyer</Const> <Var>Buyer</Var> </slot> <slot rif:ordered="yes"> <Const type="&rif;iri">&cpt;seller</Const> <Var>Seller</Var> </slot> <slot rif:ordered="yes"> <Const type="&rif;iri">&cpt;item</Const> <Expr> <op><Const type="&rif;iri">&cpt;book</Const></op> <slot rif:ordered="yes"> <Name>&cpt;author</Name> <Var>Author</Var> </slot> <slot rif:ordered="yes"> <Name>&cpt;title</Name> <Const type="&rif;iri">&bks;LeRif</Const> </slot> </Expr> </slot> <slot rif:ordered="yes"> <Const type="&rif;iri">&cpt;price</Const> <Const type="&xsd;integer">49</Const> </slot> <slot rif:ordered="yes"> <Const type="&rif;iri">&cpt;currency</Const> <Const type="&rif;iri">&curr;USD</Const> </slot> </Frame> </formula> </And> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And>
We now extend the RIF-BLD serialization from Section XML for RIF-BLD Condition Language by including rules, along with their enclosing groups and documents, as described in Section EBNF for RIF-BLD Rule Language. The extended serialization uses the following additional tags.
- Document (document, containing optional directives and payload) - directive (directive role, containing Import, Prefix, or Base) - payload (payload role, containing Group) - Import (importation, containing location and optional profile) - location (location role, containing Const of type iri) - profile (profile role, containing PROFILE) - Group (nested collection of sentences) - sentence (sentence role, containing RULE or Group) - Forall (quantified formula for 'Forall', containing declare and formula roles) - Implies (implication, containing if and then roles) - if (antecedent role, containing FORMULA) - then (consequent role, containing ATOMIC)
- id (identifier role, containing Const) - meta (meta role, containing metadata as a Frame or Frame conjunction)
The id and meta elements can occur optionally as the initial children of any Class element.
The XML Schema Definition of RIF-BLD is given in Appendix XML Schema for BLD.
Example 6 (Serializing a RIF-BLD document containing a group
annotated with metadata).
This example shows a serialization for the document from Example 3. For convenience, the document is reproduced at the top and then is followed by its serialization.
Presentation syntax: Document( Prefix(ppl http://example.com/people#) Prefix(cpt http://example.com/concepts#) Prefix(dc http://purl.org/dc/terms/) Prefix(w3 http://www.w3.org/) Prefix(rif http://www.w3.org/2007/rif#) Prefix(op http://www.w3.org/2007/rif-builtin-predicate#) Prefix(xsd http://www.w3.org/2001/XMLSchema#) (* <http://sample.org> pd[dc:publisher -> w3:W3C dc:date -> "2008-04-04"^^xsd:date] *) Group ( Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays ( cpt:reject(ppl:John ?item) :- And(cpt:perishable(?item) cpt:delivered(?item ?deliverydate ppl:John) cpt:scheduled(?item ?scheduledate) External(fn:subtract-dateTimes-yielding-dayTimeDuration(?deliverydate ?scheduledate ?diffduration)) External(fn:get-days-from-dayTimeDuration(?diffduration ?diffdays)) External(op:numeric-greater-than(?diffdays 10))) ) Forall ?item ( cpt:reject(ppl:Fred ?item) :- cpt:unsolicited(?item) ) ) ) XML syntax: <!DOCTYPE Document [ <!ENTITY ppl "http://example.com/people#"> <!ENTITY cpt "http://example.com/concepts#"> <!ENTITY dc "http://purl.org/dc/terms/"> <!ENTITY w3 "http://www.w3.org/"> <!ENTITY rif "http://www.w3.org/2007/rif#"> <!ENTITY op "http://www.w3.org/2007/rif-builtin-predicate#"> <!ENTITY xsd "http://www.w3.org/2001/XMLSchema#"> ]> <Document> <payload> <Group> <id> <Const type="&rif;iri">http://sample.org</Const> </id> <meta> <Frame> <object> <Const type="rif:local">pd</Const> </object> <slot rif:ordered="yes"> <Const type="&rif;iri">&dc;publisher</Const> <Const type="&rif;iri">&w3;W3C</Const> </slot> <slot rif:ordered="yes"> <Const type="&rif;iri">&dc;date</Const> <Const type="&xsd;date">2008-04-04</Const> </slot> </Frame> </meta> <sentence> <Forall> <declare><Var>item</Var></declare> <declare><Var>deliverydate</Var></declare> <declare><Var>scheduledate</Var></declare> <declare><Var>diffduration</Var></declare> <declare><Var>diffdays</Var></declare> <formula> <Implies> <if> <And> <formula> <Atom> <op><Const type="&rif;iri">&cpt;perishable</Const></op> <args rif:ordered="yes"><Var>item</Var></args> </Atom> </formula> <formula> <Atom> <op><Const type="&rif;iri">&cpt;delivered</Const></op> <args rif:ordered="yes"> <Var>item</Var> <Var>deliverydate</Var> <Const type="&rif;iri">&ppl;John</Const> </args> </Atom> </formula> <formula> <Atom> <op><Const type="&rif;iri">&cpt;scheduled</Const></op> <args rif:ordered="yes"> <Var>item</Var> <Var>scheduledate</Var> </args> </Atom> </formula> <formula> <External> <content> <Atom> <op><Const type="&rif;iri">&fn;subtract-dateTimes-yielding-dayTimeDuration</Const></op> <args rif:ordered="yes"> <Var>deliverydate</Var> <Var>scheduledate</Var> <Var>diffduration</Var> </args> </Atom> </content> </External> </formula> <formula> <External> <content> <Atom> <op><Const type="&rif;iri">&fn;get-days-from-dayTimeDuration</Const></op> <args rif:ordered="yes"> <Var>diffduration</Var> <Var>diffdays</Var> </args> </Atom> </content> </External> </formula> <formula> <External> <content> <Atom> <op><Const type="&rif;iri">&op;numeric-greater-than</Const></op> <args rif:ordered="yes"> <Var>diffdays</Var> <Const type="&xsd;long">10</Const> </args> </Atom> </content> </External> </formula> </And> </if> <then> <Atom> <op><Const type="&xsd;long">reject</Const></op> <args rif:ordered="yes"> <Const type="&rif;iri">&ppl;John</Const> <Var>item</Var> </args> </Atom> </then> </Implies> </formula> </Forall> </sentence> <sentence> <Forall> <declare><Var>item</Var></declare> <formula> <Implies> <if> <Atom> <op><Const type="&rif;iri">&cpt;unsolicited</Const></op> <args rif:ordered="yes"><Var>item</Var></args> </Atom> </if> <then> <Atom> <op><Const type="&rif;iri">&cpt;reject</Const></op> <args rif:ordered="yes"> <Const type="&rif;iri">&ppl;Fred</Const> <Var>item</Var> </args> </Atom> </then> </Implies> </formula> </Forall> </sentence> </Group> </payload> </Document>
We now show how to translate between the presentation and XML syntaxes of RIF-BLD.
Editor's Note: This XML syntax translation table is expected to be made more formal in future versions of this draft.
The translation between the presentation syntax and the XML syntax of the RIF-BLD Condition Language is specified by the table below. Since the presentation syntax of RIF-BLD is context sensitive, the translation must differentiate between the terms that occur in the position of the individuals from terms that occur as atomic formulas. To this end, in the translation table, the positional and named argument terms that occur in the context of atomic formulas are denoted by the expressions of the form pred(...) and the terms that occur as individuals are denoted by expressions of the form func(...).
The prime symbol (for instance, variable') indicates that the translation function defined by the table must be applied recursively (i.e., to variable in our example).
Presentation Syntax | XML Syntax |
---|---|
And ( conjunct1 . . . conjunctn ) |
<And> <formula>conjunct1'</formula> . . . <formula>conjunctn'</formula> </And> |
Or ( disjunct1 . . . disjunctn ) |
<Or> <formula>disjunct1'</formula> . . . <formula>disjunctn'</formula> </Or> |
Exists variable1 . . . variablen ( body ) |
<Exists> <declare>variable1'</declare> . . . <declare>variablen'</declare> <formula>body'</formula> </Exists> |
pred ( argument1 . . . argumentn ) |
<Atom> <op>pred'</op> <args rif:ordered="yes"> argument1' . . . argumentn' </args> </Atom> |
External ( atomicexpr ) |
<External> <content>atomicexpr'</content> </External> |
func ( argument1 . . . argumentn ) |
<Expr> <op>func'</op> <args rif:ordered="yes"> argument1' . . . argumentn' </args> </Expr> |
pred ( unicodestring1 -> filler1 . . . unicodestringn -> fillern ) |
<Atom> <op>pred'</op> <slot rif:ordered="yes"> <Name>unicodestring1</Name> filler1' </slot> . . . <slot rif:ordered="yes"> <Name>unicodestringn</Name> fillern' </slot> </Atom> |
func ( unicodestring1 -> filler1 . . . unicodestringn -> fillern ) |
<Expr> <op>func'</op> <slot rif:ordered="yes"> <Name>unicodestring1</Name> filler1' </slot> . . . <slot rif:ordered="yes"> <Name>unicodestringn</Name> fillern' </slot> </Expr> |
inst [ key1 -> filler1 . . . keyn -> fillern ] |
<Frame> <object>inst'</object> <slot rif:ordered="yes"> key1' filler1' </slot> . . . <slot rif:ordered="yes"> keyn' fillern' </slot> </Frame> |
inst # class |
<Member> <instance>inst'</instance> <class>class'</class> </Member> |
sub ## super |
<Subclass> <sub>sub'</sub> <super>super'</super> </Subclass> |
left = right |
<Equal> <side>left'</side> <side>right'</side> </Equal> |
unicodestring^^space |
<Const type="space">unicodestring</Const> |
?unicodestring |
<Var>unicodestring</Var> |
The translation between the presentation syntax and the XML syntax of the RIF-BLD Rule Language is given by the table below, which extends the translation table of Section Translation of RIF-BLD Condition Language.
Presentation Syntax | XML Syntax |
---|---|
Document( Import(loc1) . . . Import(locn) group ) |
<Document> <directive> <Import> <location>loc1'</location> </Import> </directive> . . . <directive> <Import> <location>locn'</location> </Import> </directive> <payload>group'</payload> </Document> |
Document( Import(loc1 pro1) . . . Import(locn pron) group ) |
<Document> <directive> <Import> <location>loc1'</location> <profile>pro1'</profile> </Import> </directive> . . . <directive> <Import> <location>locn'</location> <profile>pron'</profile> </Import> </directive> <payload>group'</payload> </Document> |
Group( clause1 . . . clausen ) |
<Group> <sentence>clause1'</sentence> . . . <sentence>clausen'</sentence> </Group> |
Forall variable1 . . . variablen ( rule ) |
<Forall> <declare>variable1'</declare> . . . <declare>variablen'</declare> <formula>rule'</formula> </Forall> |
conclusion :- condition |
<Implies> <if>condition'</if> <then>conclusion'</then> </Implies> |
Presentation Annotation: |
XML Annotation: |
(* const frameconj *) Classtag(. . .) |
<Classtag> <id>const'</id> <meta>frameconj'</meta> . . . </Classtag> |
Let Τ be a set of data types, which includes the data types specified in the RIF-DTB document, and suppose Ε is a set of external predicates and functions, which includes the built-ins listed in the RIF-DTB document. Let D be a RIF dialect (e.g., RIF-BLD). We say that a formula φ is a DΤ,Ε formula iff
A RIF processor is a conformant DΤ,Ε consumer iff it implements a semantics-preserving mapping, μ, from the set of all DΤ,Ε formulas to the language L of the processor.
Formally, this means that for any pair φ, ψ of DΤ,Ε formulas for which φ |=D ψ is defined, φ |=D ψ iff μ(φ) |=L μ(ψ). Here |=D denotes the logical entailment in the RIF dialect D and |=L is the logical entailment in the language L of the RIF processor. In addition, a DΤ,Ε conformant consumer must reject any document that contains a non-DΤ,Ε formula.
A RIF processor is a conformant DΤ,Ε producer iff it implements a semantics-preserving mapping, μ, from a subset of the language L of the processor to a set of DΤ,Ε formulas.
Formally this means that for any pair φ, ψ of formulas in L for which φ |=L ψ is defined, φ |=L ψ iff μ(φ) |=D μ(ψ).
RIF-BLD specific clauses: A conformant RIF-BLD
consumer is a conformant BLDΤ,Ε consumer if Τ
consists only of the datatypes and Ε consists only of the
externally defined terms that are required by RIF-BLD. These data
types and externally defined terms (called builtins) are specified
in the RIF-DTB
document. A conformant RIF-BLD consumer must reject all inputs
which do not match the syntax of BLD. If it implements extensions,
it may do so under user control -- having a "strict BLD" mode and a
"run-with-extensions" mode.
A conformant BLD producer produces documents that include only the datatypes and externals that are required by BLD.
A conformant BLD document is one which conforms to all the syntactic constraints of this RIF-BLD specification, including ones that cannot be checked by XML Schema validator.
RIF-BLD round-tripping: A round-tripping of a
conformant BLD document is its semantics-preserving mapping
to a document in any language L followed by a
semantics-preserving mapping from the L document back to a
conformant BLD document. While semantically equivalent, the
original and the round-tripped BLD documents need not be
identical.
Metadata SHOULD survive BLD round-tripping.
This normative section describes RIF-BLD by specializing RIF-FLD. The reader is assumed to be familiar with RIF-FLD as described in RIF Framework for Logic-Based Dialects. The reader who is not interested in how RIF-BLD is derived from the framework can skip this section.
This section defines the precise relationship between the presentation syntax of RIF-BLD and the syntactic framework of RIF-FLD.
The presentation syntax of the RIF Basic Logic Dialect is defined by specialization from the presentation syntax of the RIF Syntactic Framework for Logic Dialects. Section Syntax of a RIF Dialect as a Specialization of the RIF Framework in that document lists the parameters of the syntactic framework in mathematical English, which we will now specialize for RIF-BLD.
The signature set of RIF-BLD contains the following signatures:
The signature individual{ } represents the context
in which individual objects (but not atomic formulas) can
appear.
The signature atomic{ } represents the context where
atomic formulas can occur.
These represent function and predicate symbols of arity n (each of the above cases has n individuals as arguments inside the parentheses).
Thus, in RIF-BLD each constant symbol can be either an individual, a function of one particular arity or with certain argument names, a predicate of one particular arity or with certain argument names, an externally defined function of one particular arity, or an externally defined predicate symbol of one particular arity -- it is not possible for the same symbol to play more than one role.
This means that equality can compare only those terms whose signature is individual; it cannot compare predicate names or function symbols. Equality terms are also not allowed to occur inside other terms, since the above signature implies that any term of the form t = s has signature atomic and not individual.
Note that this precludes the possibility that a frame term might occur as an argument to a predicate, a function, or inside some other term.
Note that this precludes the possibility that a membership term might occur as an argument to a predicate, a function, or inside some other term.
As with frames and membership terms, this precludes the possibility that a subclass term might occur inside some other term.
RIF-BLD uses no special syntax for declaring signatures. Instead, the author specifies signatures contextually. That is, since RIF-BLD requires that each symbol is associated with a unique signature, the signature is determined from the context in which the symbol is used. If a symbol is used in more than one context, the parser must treat this as a syntax error. If no errors are found, all terms and atomic formulas are guaranteed to be well-formed. Thus, signatures are not part of the RIF-BLD language, and individual and atomic are not reserved keywords in RIF-BLD.
RIF-BLD supports all the symbol spaces defined in Section Constants and Symbol Spaces of the document Data Types and Built-Ins.
RIF-BLD supports the following types of formulas (see Well-formed Terms and Formulas for the definitions):
A RIF-BLD condition is an atomic formula, a conjunctive or disjunctive combination of atomic formulas with optional existential quantification of variables, or an external atomic formula.
A RIF-BLD rule is a universally quantified RIF-FLD rule with the following restrictions:
A RIF-BLD group is a RIF-FLD group that contains only RIF-BLD rules and RIF-BLD groups.
A RIF-BLD document is a RIF-FLD document that consists of directives and a RIF-BLD group formula. The import-directives are allowed to import only RIF-BLD documents.
Recall that negation (classical or default) is not supported by RIF-BLD in either the rule head or the body.
This normative section defines the precise relationship between the semantics of RIF-BLD and the semantic framework of RIF-FLD. Specification of the semantics that does not rely on RIF-FLD is given in Section Direct Specification of RIF-BLD Semantics.
The semantics of the RIF Basic Logic Dialect is defined by specialization from the semantics of the Semantic Framework for Logic Dialects of RIF. Section Semantics of a RIF Dialect as a Specialization of the RIF Framework in that document lists the parameters of the semantic framework, which one need to specialize. Thus, for RIF-BLD, we need to look at the following parameters:
RIF-BLD does not support negation. This is the only obvious simplification with respect to RIF-FLD as far as the semantics is concerned. The restrictions on the signatures of symbols in RIF-BLD do not affect the semantics in a significant way.
The set TV of truth values in RIF-BLD consists of just two values, t and f such that f <t t. The order <t is total.
RIF-BLD supports all the data types listed in Section Data Types of the document Data Types and Builtins.
Recall that logical entailment in RIF-FLD is defined with respect to an unspecified set of intended semantic structures and that dialects of RIF must make this notion concrete. For RIF-BLD, this set is defined in one of the two following equivalent ways:
These two definitions are equivalent for entailment of existentially closed RIF-BLD conditions by RIF-BLD documents (i.e., formulas where every variable, ?V, occurs in a subformula of the form Exists ...?V...(ψ)), since all rules in RIF-BLD are Horn -- it is a classical result of Van Emden and Kowalski [vEK76].
The namespace of RIF is http://www.w3.org/2007/rif#.
XML schemas for the RIF-BLD sublanguages are available below and online, with examples.
<?xml version="1.0" encoding="UTF-8"?> <xs:schema xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns="http://www.w3.org/2007/rif#" targetNamespace="http://www.w3.org/2007/rif#" elementFormDefault="qualified" version="Id: BLDCond.xsd,v 0.8 2008-04-14 dhirtle/hboley"> <xs:annotation> <xs:documentation> This is the XML schema for the Condition Language as defined by Working Draft 2 of the RIF Basic Logic Dialect. The schema is based on the following EBNF for the RIF-BLD Condition Language: FORMULA ::= 'And' '(' FORMULA* ')' | 'Or' '(' FORMULA* ')' | 'Exists' Var+ '(' FORMULA ')' | ATOMIC | 'External' '(' ATOMIC ')' ATOMIC ::= Atom | Equal | Member | Subclass | Frame Atom ::= UNITERM UNITERM ::= Const '(' (TERM* | (Name '->' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '->' TERM)* ']' TERM ::= Const | Var | Expr | 'External' '(' Expr ')' Expr ::= UNITERM Const ::= '"' UNICODESTRING '"^^' SYMSPACE Name ::= UNICODESTRING Var ::= '?' UNICODESTRING </xs:documentation> </xs:annotation> <xs:group name="FORMULA"> <xs:choice> <xs:element ref="And"/> <xs:element ref="Or"/> <xs:element ref="Exists"/> <xs:group ref="ATOMIC"/> <xs:element name="External" type="External-FORMULA.type"/> </xs:choice> </xs:group> <xs:complexType name="External-FORMULA.type"> <xs:sequence> <xs:element name="content" type="content-FORMULA.type"/> </xs:sequence> </xs:complexType> <xs:complexType name="content-FORMULA.type"> <xs:sequence> <xs:group ref="ATOMIC"/> </xs:sequence> </xs:complexType> <xs:element name="And"> <xs:complexType> <xs:sequence> <xs:element ref="formula" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Or"> <xs:complexType> <xs:sequence> <xs:element ref="formula" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Exists"> <xs:complexType> <xs:sequence> <xs:element ref="declare" minOccurs="1" maxOccurs="unbounded"/> <xs:element ref="formula"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="formula"> <xs:complexType> <xs:sequence> <xs:group ref="FORMULA"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="declare"> <xs:complexType> <xs:sequence> <xs:element ref="Var"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="ATOMIC"> <xs:choice> <xs:element ref="Atom"/> <xs:element ref="Equal"/> <xs:element ref="Member"/> <xs:element ref="Subclass"/> <xs:element ref="Frame"/> </xs:choice> </xs:group> <xs:element name="Atom"> <xs:complexType> <xs:sequence> <xs:group ref="UNITERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="UNITERM"> <xs:sequence> <xs:element ref="op"/> <xs:choice> <xs:element ref="arg" minOccurs="0" maxOccurs="unbounded"/> <xs:element name="slot" type="slot-UNITERM.type" minOccurs="0" maxOccurs="unbounded"/> </xs:choice> </xs:sequence> </xs:group> <xs:element name="op"> <xs:complexType> <xs:sequence> <xs:element ref="Const"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="arg"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:complexType name="slot-UNITERM.type"> <xs:sequence> <xs:element name="Prop" type="Prop-UNITERM.type"/> </xs:sequence> </xs:complexType> <xs:complexType name="Prop-UNITERM.type"> <xs:sequence> <xs:element name="key" type="key-UNITERM.type"/> <xs:element ref="val"/> </xs:sequence> </xs:complexType> <xs:complexType name="key-UNITERM.type"> <xs:sequence> <xs:element ref="Name"/> </xs:sequence> </xs:complexType> <xs:element name="val"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Equal"> <xs:complexType> <xs:sequence> <xs:element ref="side"/> <xs:element ref="side"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="side"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Member"> <xs:complexType> <xs:sequence> <xs:element ref="lower"/> <xs:element ref="upper"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Subclass"> <xs:complexType> <xs:sequence> <xs:element ref="lower"/> <xs:element ref="upper"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="lower"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="upper"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Frame"> <xs:complexType> <xs:sequence> <xs:element ref="object"/> <xs:element name="slot" type="slot-Frame.type" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="object"> <xs:complexType> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:complexType name="slot-Frame.type"> <xs:sequence> <xs:element name="Prop" type="Prop-Frame.type"/> </xs:sequence> </xs:complexType> <xs:complexType name="Prop-Frame.type"> <xs:sequence> <xs:element name="key" type="key-Frame.type"/> <xs:element ref="val"/> </xs:sequence> </xs:complexType> <xs:complexType name="key-Frame.type"> <xs:sequence> <xs:group ref="TERM"/> </xs:sequence> </xs:complexType> <xs:group name="TERM"> <xs:choice> <xs:element ref="Const"/> <xs:element ref="Var"/> <xs:element ref="Expr"/> <xs:element name="External" type="External-TERM.type"/> </xs:choice> </xs:group> <xs:complexType name="External-TERM.type"> <xs:sequence> <xs:element name="content" type="content-TERM.type"/> </xs:sequence> </xs:complexType> <xs:complexType name="content-TERM.type"> <xs:sequence> <xs:element ref="Expr"/> </xs:sequence> </xs:complexType> <xs:element name="Expr"> <xs:complexType> <xs:sequence> <xs:group ref="UNITERM"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Const"> <xs:complexType mixed="true"> <xs:sequence/> <xs:attribute name="type" type="xs:string" use="required"/> </xs:complexType> </xs:element> <xs:element name="Name" type="xs:string"> </xs:element> <xs:element name="Var" type="xs:string"> </xs:element> </xs:schema>
<?xml version="1.0" encoding="UTF-8"?> <xs:schema xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns="http://www.w3.org/2007/rif#" targetNamespace="http://www.w3.org/2007/rif#" elementFormDefault="qualified" version="Id: BLDRule.xsd,v 0.8 2008-04-09 dhirtle/hboley"> <xs:annotation> <xs:documentation> This is the XML schema for the Rule Language as defined by Working Draft 2 of the RIF Basic Logic Dialect. The schema is based on the following EBNF for the RIF-BLD Rule Language: Document ::= Group Group ::= 'Group' IRIMETA? '(' (RULE | Group)* ')' IRIMETA ::= Frame RULE ::= 'Forall' Var+ '(' CLAUSE ')' | CLAUSE CLAUSE ::= Implies | ATOMIC Implies ::= ATOMIC ':-' FORMULA Note that this is an extension of the syntax for the RIF-BLD Condition Language (BLDCond.xsd). </xs:documentation> </xs:annotation> <xs:include schemaLocation="BLDCond.xsd"/> <xs:element name="Document"> <xs:complexType> <xs:sequence> <xs:element ref="Group"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Group"> <xs:complexType> <xs:sequence> <xs:element ref="meta" minOccurs="0" maxOccurs="1"/> <xs:element ref="sentence" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="meta"> <xs:complexType> <xs:sequence> <xs:group ref="IRIMETA"/> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="IRIMETA"> <xs:sequence> <xs:element ref="Frame"/> </xs:sequence> </xs:group> <xs:element name="sentence"> <xs:complexType> <xs:choice> <xs:element ref="Group"/> <xs:group ref="RULE"/> </xs:choice> </xs:complexType> </xs:element> <xs:group name="RULE"> <xs:choice> <xs:element ref="Forall"/> <xs:group ref="CLAUSE"/> </xs:choice> </xs:group> <xs:element name="Forall"> <xs:complexType> <xs:sequence> <xs:element ref="declare" minOccurs="1" maxOccurs="unbounded"/> <xs:element name="formula"> <xs:complexType> <xs:group ref="CLAUSE"/> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element> <xs:group name="CLAUSE"> <xs:choice> <xs:element ref="Implies"/> <xs:group ref="ATOMIC"/> </xs:choice> </xs:group> <xs:element name="Implies"> <xs:complexType> <xs:sequence> <xs:element ref="if"/> <xs:element ref="then"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="if"> <xs:complexType> <xs:sequence> <xs:group ref="FORMULA"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="then"> <xs:complexType> <xs:sequence> <xs:group ref="ATOMIC"/> </xs:sequence> </xs:complexType> </xs:element> </xs:schema>