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:
- As a specialization of the RIF Framework for Logic-based Dialects (RIF-FLD),
which is part of the RIF extensibility framework.
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.
- Independently of the RIF framework for logic dialects, for the
benefit of those who desire a quicker path to RIF-BLD, e.g. as
prospective implementers, and are not interested in the
extensibility issues. This version of the RIF-BLD specification is
given first.
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.
Editor's Note: This document is the latest draft of the RIF-BLD specification. A number of extensions is planned to support import of RIF documents, the notion of RIF compliance, and a few others. Tool support for RIF-BLD is forthcoming.2 Direct Specification of RIF-BLD
Presentation Syntax
This normative section specifies the syntax of RIF-BLD directly,
without relying on RIF-FLD. We define both athe 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.
Editor's Note: A future version of this document might introduce syntactic shortcutsNote to simplify writingthe examplesreader: this section depends on Section Constants, Symbol
Spaces, and Data Types of the document Data Types and test cases.Builtins.
2.1 Alphabet of RIF-BLD
Definition
(Alphabet). The alphabet of the presentation
language of RIF-BLD consists of
- a countably infinite set of constant symbols
Const
- a countably infinite set of variable symbols
Var (disjoint from Const)
- a countably infinite set of argument names, ArgNames
(disjoint from Const and Var)
- connective symbols And, Or, and
:-
- quantifiers Exists and Forall
- the symbols =, #, ##,
->,
andExternal, Prefix,
Base
- the symbols Document, Group, and
Import
- auxiliary symbols, such as "(", ")", "[", "]", and "^^"
The set of connective symbols, quantifiers, =, etc., is
disjoint from Const and Var. The argument names
in ArgNames are written as unicode strings that must not
start with a question mark, "?". Variables are written as
Unicode strings preceded with the symbol "?".
Constants are written as "literal"^^symspace, where
literal is a sequence of Unicode characters and
symspace is an identifier for a symbol space. Symbol
spaces are defined in Section Constants and
Symbol Spaces of the RIF-FLD document . Editor's Note: The definition of symbol spaces will eventually be also given in thedocument Data Types and Builtins , so the above reference will be to that document instead of RIF-FLD..
The symbols =, #, and ## are used in
formulas that define equality, class membership, 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).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 optionally annotated with metadata.collections. ☐
The language of RIF-BLD is the set of formulas constructed using
the above alphabet according to the rules given below.
2.2 Terms
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:
- Internal base term: A simple, positional, or
named-argument term.
-
ExternalBase term: An externalinternal base term of the formor
External(t), where
t is an internal base term. Internal term : Everything but an external term (i.e., internal base, equality, membership, subclass, and frame terms). Base term : An internala positional or external basea named-argument term.
Definition
(Term).
- Constants and variables. If t ∈ Const
or t ∈ Var then t is a simple
term.
- Positional terms. If t ∈ Const and
t1, ..., tn are base terms
then t(t1 ... tn) is a
positional term.
- Terms with named arguments. A term with named
arguments is of the form
t(s1->v1 ...
sn->vn), where t ∈
Const and v1, ...,
vn are base terms and s1,
..., sn are pairwise distinct symbols from the
set ArgNames.
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.
- Equality terms. If t and s are base
terms then t = s is an equality
term.
- Class membership terms (or just membership
terms). t#s is a membership term if
t and s are base terms.
- Subclass terms. t##s is a subclass
term if t and s are base terms.
- Frame terms. t[p1->v1 ...
pn->vn] is a frame term
(or simply a frame) if t,
p1, ..., pn,
v1, ..., vn, n ≥
0, are base terms.
Membership, subclass, and frame terms are used to describe
objects and class hierarchies.
- Externally defined terms. If t is
an internal non-variablea positional,
named-argument, or a frame term then External(t) is an
externally defined term.
-
Such terms are used for representing builtin functions and
predicates as well as "procedurally attached" terms or predicates,
which might exist in various 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.
2.3 Well-formedness of Terms
The set of all symbols, Const, is partitioned into
Each predicate and function symbol has precisely one
arity.
- For positional symbols, an arity is a non-negative integer that
tells how many arguments the symbol can take.
- For symbols that take named arguments, an arity is a set
{s1 ... sk} of argument names
(si ∈ ArgNames) that are allowed for
that symbol.
The arity of a symbol (or whether it is a predicate, a function,
or an individual) is not specified in 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:
- An individual.
This means that p is a term by itself, which appears
inside some other term (positional, with named arguments, in a
frame, etc.).
- A function symbol of a particular arity.
This means that p occurs in a term t of the
form p(...) and t itself occurs inside some other
term.
- A predicate symbol of a particular arity.
This means that p occurs in a term t of the
form p(...) and t does not occur inside some
other term.
The arity of the symbol and its type is determined by its
context. If a symbol from Const occurs in more than one
context in a set of formulas, the set is not
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 RIF-FLD.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.
Editor's Note: The definition of external schemas will eventually also appear in the document Data Types and Builtins , so the above reference will be to that document instead of RIF-FLD.A well-formed
term is one that occurs in a well-formed set of
fomulas.
2.4 Formulas
Any term (positional or with named arguments) of the form
p(...), where p is a predicate symbol, is also an
atomic formula. Equality, membership, subclass, and
frame terms are also atomic formulas. 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:
- Atomic: If φ is a well-formed atomic formula
then it is also a well-formed formula.
- Condition formula: A
condition formula is either an atomic formula or a
formula that has one of the following forms:
- Conjunction: If φ1, ...,
φn, n ≥ 0, are well-formed condition
formulas then so is And(φ1 ... φn),
called a conjunctive formula. As a special case,
And() is allowed and is treated as a tautology, i.e., a
formula that is always true.
- Disjunction: If φ1, ...,
φn, n ≥ 0, are well-formed condition
formulas then so is Or(φ1 ... φn),
called a disjunctive formula. When n=0, we get
Or() as a special case; it is treated as a contradiction,
i.e., a formula that is always false.
- Existentials: If φ is a well-formed condition
formula and ?V1, ..., ?Vn
are variables then Exists ?V1
... ?Vn(φ) is an existential
formula.
Condition formulas constructed using the above definitionsare called RIF-BLD conditions .intended to be used inside the following definespremises
of rules. Next we define the notion of a RIF-BLD rule.rule, sets of
rules, and RIF documents.
It can be seen fromThe above definitions thatendow RIF-BLD haswith a wide variety of
syntactic forms for terms and formulas. This provides theformulas, which creates
infrastructure for exchanging syntactically diverse rule languages that support rich collections of syntactic forms.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).
2.5 EBNF Grammar forMetadata in the Presentation
Syntax
ofRIF-BLD So far, the syntaxallows every term to be optionally preceded by a
metadata block of RIF-BLD has been specified in mathematical English. Tool developers, however, may prefer EBNF notation, which providesthe form (* id φ *) where
id is a more succinct overviewrif:iri constant and φ is a
frame formula or a conjunction of frame formulas. Both items inside
the syntax. Several points should be kept in mind regarding this notation.metadata block are optional. The syntax of first-order logic is not context-free, so EBNF does not captureid part represents
the syntaxmeta-identifier of RIF-BLD precisely. For instance, it cannot capturethe section on well-formedness conditions , i.e.,term to which the requirement that each symbol in RIF-BLD canmetadata 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.
2.6 EBNF Grammar for the Presentation
Syntax of RIF-BLD
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 syntax of first-order logic is not context-free, so EBNF
cannot capture the syntax of RIF-BLD precisely. For instance, it
cannot capture the section on well-formedness conditions, i.e., the requirement that each
symbol in RIF-BLD can occur in at most one context. As a result,
the EBNF grammar defines a strict superset of RIF-BLD (not
all rules that are derivable using the EBNF grammar are well-formed
rules in RIF-BLD).
- The EBNF
syntax is not a concrete syntax: itgrammar does not address the details of how constants
and variables are represented, and it is not sufficiently precise
about the delimiters and escape symbols. Instead, white space is
informally used as athe delimiter, and white space is implied in
productions that use Kleene star. For instance, TERM* is
to be understood as TERM TERM ... TERM,
where each ' ' abstracts from one or more blanks, tabs, newlines,
etc. This is done intentionally, sinceso because RIF's presentation syntax is used asa tool for
specifying the semantics and for illustration of the main RIF
concepts through examples. It is not intended as a concrete
syntax for a rule language. RIF defines a concrete syntax only for
exchanging rules, and that syntax is XML-based, obtained as
a refinement and serialization of the EBNFpresentation syntax.
- For all the above reasons, the EBNF
syntaxgrammar is not
normative. 2.5.1(The non-normative status of the EBNF grammer should
not be confused with the normative status of the RIF-BLD
presentation syntax.)
2.6.1 EBNF for the RIF-BLD Condition
Language
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' '(' ATOMICAtom | 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( ATOMICAtom) is a
call to an externally defined predicate;
External(Frame) is a call to an externally
defined predicate, equality, membership, subclassing, orframe. 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 compact URIshortcut notation
[ CURIE ],prefix:suffix, which should be understood as a macro that
expands into aan 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 should be understood merely asis an
abbreviation for
http://example.com/books#LeRif"http://example.com/books#LeRif"^^rif:iri. This and other
shortcuts are defined in the compact URI notation is not part ofdocument Data Types and Builtins.
Assume that the RIF-BLD syntax. Compact URI prefixes: bks expands into http://example.com/books# auth expands into http://example.com/authors# cpt expands into http://example.com/concepts#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"^^rif:iri("auth:rifwg"^^rif:iri "bks:LeRif"^^rif:iri)cpt:book(auth:rifwg bks:LeRif)
Exists ?X ("cpt:book"^^rif:iri(?X "bks:LeRif"^^rif:iri))(cpt:book(?X bks:LeRif))
Terms with named arguments:
"cpt:book"^^rif:iri(cpt:author->"auth:rifwg"^^rif:iri cpt:title->"bks:LeRif"^^rif:iri)cpt:book(cpt:author->auth:rifwg cpt:title->bks:LeRif)
Exists ?X ("cpt:book"^^rif:iri(cpt:author->?X cpt:title->"bks:LeRif"^^rif:iri))(cpt:book(cpt:author->?X cpt:title->bks:LeRif))
Frames:
"bks:wd1"^^rif:iri["cpt:author"^^rif:iri->"auth:rifwg"^^rif:iri "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]bks:wd1[cpt:author->auth:rifwg cpt:title->bks:LeRif]
Exists ?X ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri])(bks:wd2[cpt:author->?X cpt:title->bks:LeRif])
Exists ?X (And ("bks:wd2"^^rif:iri#"cpt:book"^^rif:iri "bks:wd2"^^rif:iri["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]))(bks:wd2#cpt:book bks:wd2[cpt:author->?X cpt:title->bks:LeRif]))
Exists ?I ?X (?I["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri])(?I[cpt:author->?X cpt:title->bks:LeRif])
Exists ?I ?X (And (?I#"cpt:book"^^rif:iri ?I["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]))(?I#cpt:book ?I[cpt:author->?X cpt:title->bks:LeRif]))
Exists ?S ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->"auth:rifwg"^^rif:iri ?S->"bks:LeRif"^^rif:iri])(bks:wd2[cpt:author->auth:rifwg ?S->bks:LeRif])
Exists ?X ?S ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->?X ?S->"bks:LeRif"^^rif:iri])(bks:wd2[cpt:author->?X ?S->bks:LeRif])
Exists ?I ?X ?S (And (?I#"cpt:book"^^rif:iri(?I#cpt:book ?I[author->?X ?S->"bks:LeRif"^^rif:iri])) 2.5.2?S->bks:LeRif]))
2.6.2 EBNF for the RIF-BLD Rule
Language
The presentation syntax for RIF-BLD rules extends the syntax in
Section EBNF for
RIF-BLD Condition Language with the following productions.
Editor's Note: The metadata syntax and the approach to rule identification presented in this draft are currently under discussion by the Working Group. Input is welcome. See Issue-51Document ::= IRIMETA? 'Document' '(' IRIMETA?DIRECTIVE* Group? ')'
DIRECTIVE ::= Import | Prefix | Base
Import ::= 'Import' '(' IRI PROFILE? ')'
Prefix ::= 'Prefix' '(' Name IRI ')'
Base ::= 'Base' '(' IRI ')'
Group ::= 'Group'IRIMETA? 'Group' '(' (RULE | Group)* ')'
IRIMETA ::= FrameRULE ::= 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 annotated with optional metadata, IRIMETA .main part. A DIRECTIVE can containbe any number of
Imports, Prefixes, or Bases. A RIF-BLD
Group is a nested collection of RIF-BLD rules annotated with optional metadata, IRIMETA . IRIMETA are represented as Frame s. A Group can containany 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:
If an item is perishable and it
is delivered to John more than 10 days after the scheduled delivery
date then the item will be rejected by him.
As before, for better readability we use the compact URI
notation. Compact URI prefixes: ppl expands into http://example.com/people# cpt expands into http://example.com/concepts# op expands intonotation defined in [[DTB|Data Types and Builtins, Section Constants and
Symbol Spaces. Again, prefix directives are assumed in the
yet-to-be-determined IRI for RIF builtin predicatespreamble 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"^^rif:iri("ppl:John"^^rif:iricpt:reject(ppl:John ?item) :-
And("cpt:perishable"^^rif:iri(?item) "cpt:delivered"^^rif:iri(?itemAnd(cpt:perishable(?item)
cpt:delivered(?item ?deliverydate "ppl:John"^^rif:iri) "cpt:scheduled"^^rif:iri(?itemppl:John)
cpt:scheduled(?item ?scheduledate)
External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydateExternal(fn:subtract-dateTimes-yielding-dayTimeDuration(?deliverydate ?scheduledate ?diffduration))
External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffdurationExternal(fn:get-days-from-dayTimeDuration(?diffduration ?diffdays))
External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))External(op:numeric-greater-than(?diffdays 10)))
)
b. Universal-existential form:
Forall ?item (
"cpt:reject"^^rif:iri("ppl:John"^^rif:iricpt:reject(ppl:John ?item ) :-
Exists ?deliverydate ?scheduledate ?diffduration ?diffdays (
And("cpt:perishable"^^rif:iri(?item) "cpt:delivered"^^rif:iri(?itemAnd(cpt:perishable(?item)
cpt:delivered(?item ?deliverydate "ppl:John"^^rif:iri) "cpt:scheduled"^^rif:iri(?itemppl:John)
cpt:scheduled(?item ?scheduledate)
External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydateExternal(fn:subtract-dateTimes-yielding-dayTimeDuration(?deliverydate ?scheduledate ?diffduration))
External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffdurationExternal(fn:get-days-from-dayTimeDuration(?diffduration ?diffdays))
External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))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 represented as a frame. Compact URI prefixes: ppl expands into http://example.com/people# cpt expands into http://example.com/concepts# dc expands into http://purl.org/dc/terms/ w3 expands into http://www.w3.org/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
" http://sample.org "^^rif:iri["dc:publisher"^^rif:iri->"w3:W3C"^^rif:iri "dc:date"^^rif:iri->"2008-04-04"^^xsd:date](
Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays (
"cpt:reject"^^rif:iri("ppl:John"^^rif:iricpt:reject(ppl:John ?item) :-
And("cpt:perishable"^^rif:iri(?item) "cpt:delivered"^^rif:iri(?itemAnd(cpt:perishable(?item)
cpt:delivered(?item ?deliverydate "ppl:John"^^rif:iri) "cpt:scheduled"^^rif:iri(?itemppl:John)
cpt:scheduled(?item ?scheduledate)
External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydateExternal(fn:subtract-dateTimes-yielding-dayTimeDuration(?deliverydate ?scheduledate ?diffduration))
External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffdurationExternal(fn:get-days-from-dayTimeDuration(?diffduration ?diffdays))
External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))External(op:numeric-greater-than(?diffdays 10)))
)
Forall ?item (
"cpt:reject"^^rif:iri("ppl:Fred"^^rif:iricpt:reject(ppl:Fred ?item) :- "cpt:unsolicited"^^rif:iri(?item)cpt:unsolicited(?item)
)
)
)
3 Direct Specification of RIF-BLD
Semantics
This normative section specifies the semantics of RIF-BLD
directly, without relying on RIF-FLD.
3.1 Truth ValuesRecall 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.
3.1 Truth Values
The set TV of truth values in RIF-BLD consists of
just two values, t and f.
3.2 Semantic Structures
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 thea set of identifiers for primitive data
types used in I(please refer to Section PrimitiveData Types of
RIF-FLD for the semantics of data types). Editor's Note: In the future versions of this document, the above reference will point tothe document Data Types
and Builtins insteadfor the semantics of RIF-FLD.data types).
The other components of I are total
mappings defined as follows:
- IC maps Const to
D.
This mapping interprets constant symbols. In addition:
-
- If a constant, c ∈ Const, denotes
an individual then it is required that
IC(c) ∈ Dind.
- If c ∈ Const, denotes a function
symbol (positional or with named arguments) then it is required
that
IC(c) ∈ Dfunc.
- IV maps Var to
Dind.
This mapping interprets variable symbols.
- IF maps D to functions
D*ind → D (here
D*ind is a set of all sequences of any
finite length over the domain Dind)
This mapping interprets positional terms. In addition:
-
- If d ∈ Dfunc then
IF(d) must be a function
D*ind →
Dind.
- This means that when a function symbol is applied to arguments
that are individual objects then the result is also an individual
object.
- ISF maps D to the set of
total functions of the form
SetOfFiniteSets(ArgNames ×
Dind) → D.
This mapping interprets function symbols with named arguments.
In addition:
-
- If d ∈ Dfunc then
ISF(d) must be a function
SetOfFiniteSets(ArgNames ×
Dind) →
Dind.
- This is analogous to the interpretation of positional terms
with two differences:
-
- Each pair <s,v> ∈ ArgNames ×
Dind represents an argument/value pair
instead of just a value in the case of a positional term.
- The arguments of a term with named arguments constitute a
finite set of argument/value pairs rather than a finite ordered
sequence of simple elements. So, the order of the arguments does
not matter.
- Iframe maps
Dind to total functions of the form
SetOfFiniteBags(Dind ×
Dind) → D.
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.
- Isub gives meaning to the subclass
relationship. It is a mapping of the form
Dind × Dind →
D.
The operator ## is required to be transitive, i.e.,
c1 ## c2 and c2 ## c3 must
imply c1 ## c3. This is ensured by a restriction
in Section Interpretation of Formulas.
- Iisa gives meaning to class
membership. It is a mapping of the form
Dind × Dind →
D.
The relationships # and ## are required to
have the usual property that all members of a subclass are also
members of the superclass, i.e., o # cl and
cl ## scl must imply o # scl.
This is ensured by a restriction in Section Interpretation of
Formulas.
- I= is a mapping of the form
Dind × Dind →
D.
It gives meaning to the equality operator.
- Itruth is a mapping of the form
D → TV.
It is used to define truth valuation for formulas.
- Iexternal is a mapping from the
coherent set of schemas for externally defined functions to total
functions D* → D. For each external
schema σ = (?X1
... ?Xn; τ) in the coherent
set of such schemas associated with the language,
Iexternal(σ) is a function of the
form Dn → D.
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:
- If σ is a schema of a builtin function then
Iexternal(σ) must be the function
defined in the aforesaid document.
- If σ is a schema of a builtin predicate then
Itruth ο
(Iexternal(σ)) (the composition
of Itruth and
Iexternal(σ), a truth-valued
function) must be as specified in Data Types and Builtins.
For convenience, we also define the following mapping
I from terms to D:
- I(k) =
IC(k), if k is a symbol
in Const
- I(?v) =
IV(?v), if ?v is a
variable in Var
- I(f(t1 ... tn)) =
IF(I(f))(I(t1),...,I(tn))
- I(f(s1->v1 ...
sn->vn)) =
ISF(I(f))({<s1,I(v1)>,...,<sn,I(vn)>})
-
Here we use {...} to denote a set of argument/value pairs.
- I(o[a1->v1 ...
ak->vk]) =
Iframe(I(o))({<I(a1),I(v1)>,
...,
<I(an),I(vn)>})
-
Here {...} denotes a bag of attribute/value pairs.
- I(c1##c2) =
Isub(I(c1),
I(c2))
- I(o#c) =
Iisa(I(o),
I(c))
- I(x=y) =
I=(I(x),
I(y))
- I(External(t)) =
Iexternsl(σ)(I(s1),
..., I(sn)), if t is an
instance of the external schema σ = (?X1
... ?Xn; τ) by substitution
?X1/s1
... ?Xn/s1.
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 RIF-FLD).the document Data Types and Builtins). Then the following must
hold:
- VSdt ⊆ Dind;
and
- For each constant "lit"^^dt such that lit ∈
LSdt,
IC("lit"^^dt) =
Ldt(lit).
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.
☐
3.3 Metadata and Semantics
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.
3.4 Interpretation of Non-document
Formulas
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:
- Positional atomic formulas:
TValI(r(t1 ...
tn)) =
Itruth(I(r(t1
... tn)))
- Atomic formulas with named arguments:
TValI(p(s1->v1 ...
sk->vk)) =
Itruth(I(p(s1->v1
... sk->vk))).
- Equality:
TValI(x = y) =
Itruth(I(x = y)).
- Subclass:
TValI(sc ## cl) =
Itruth(I(sc ## cl)).
To ensure that the operator ## is transitive, i.e.,
c1 ## c2 and c2 ## c3 imply
c1 ## c3, the following is required:
For all c1, c2,
c3 ∈ D, if
TValI(c1 ## c2) =
TValI(c2 ## c3) = t
then TValI(c1 ## c3) =
t.
- Membership:
TValI(o # cl) =
Itruth(I(o # cl)).
To ensure that all members of a subclass are also members of the
superclass, i.e., o # cl and
cl ## scl implies o # scl,
the following is required:
For all o, cl,
scl ∈ D, if
TValI(o # cl) =
TValI(cl ## scl) = t
then
TValI(o # scl) =
t.
- Frame:
TValI(o[a1->v1 ...
ak->vk]) =
Itruth(I(o[a1->v1
... ak->vk])).
Since the bag of attribute/value pairs represents the
conjunctions of all the pairs, the following is required:
TValI(o[a1->v1 ...
ak->vk]) = t if and only if
TValI(o[a1->v1])
= ... =
TValI(o[ak->vk])
= t.
- Externally defined atomic formula:
TValI(External(t)) =
Itruth(Iexternal(σ)(I(s1),
..., I(sn))), if t is an
atomic formula that is an instance of the external schema σ =
(?X1 ... ?Xn; τ) by substitution
?X1/s1
... ?Xn/s1.
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.
- Conjunction:
TValI(And(c1 ...
cn)) = t if and only if
TValI(c1) = ... =
TValI(cn) = t. Otherwise,
TValI(And(c1 ...
cn)) = f.
-
The empty conjunction is treated as a tautology, so
TValI(And()) = t.
- Disjunction:
TValI(Or(c1 ...
cn)) = f if and only if
TValI(c1) = ... =
TValI(cn) = f. Otherwise,
TValI(Or(c1 ...
cn)) = t.
-
The empty disjunction is treated as a contradiction, so
TValI(Or()) = f.
- Quantification:
- TValI(Exists ?v1
... ?vn (φ)) = t if and only if for
some I*, described below,
TValI*(φ) = t.
- TValI(Forall ?v1
... ?vn (φ)) = t if and only if for
every I*, described below,
TValI*(φ) = t.
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.
- Rule implication:
- TValI(conclusion :-
condition) = t, if either
TValI(conclusion)=t or
TValI(condition)=f.
- TValI(conclusion :-
condition) = f otherwise.
- Groups of rules:
If Γ is a group formula of the form
Group φ (ρ 1 ... ρ n ) or Group (ρGroup(ρ1 ... ρn) then
- TValI(Γ) = t if and only if
TValI(ρ1) = t, ...,
TValI(ρn) = t.
- TValI(Γ) = f
otherwise.
This means that a group of rules is treated as a conjunction.
The metadata is ignored for purposes of the RIF-BLD semantics. A model of a group formula, Γ , is a semantic structure I such that TVal I ( Γ ) = t . In this case, we write I |= Γ . ☐
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. 3.43.5 Interpretation of
Documents
Document formulas are interpreted using semantic
multi-structures.
Definition (Semantic multi-structures). A semantic
multi-structure is a tuple (set
{IΔ1, ...,
IΔn ),}, n>0, where
IΔ1, ...,
IΔn are semantic
structures, which arestructures labeled with document formulas. These structures must be
identical in all respects except that the mappings
I 1CΔ1, ...,
I nC mayΔ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 samesay 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 0Δ,
IΔ1, ...,
I n )Δk, ...} be a
semantic multi-structure such that n≥k.multi-structure, which contains semantic structures
labeled with at least the documents Δ,
Δ1, ..., Δk. Then we
define:
TValI(Δ) =
t if and only if
TValI 0Δ(Γ) =
TValIΔ1(Γ1)
= ... =
TValIΔk(Γk)
= t.
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.
A model of a document formula Δ is a semantic multi-structure I such that TVal I ( Δ ) = t . In this case, we write I |= Δ . 3.53.6 Logical Entailment
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. We say that aIn
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 existentially closed , if and onlyassumed to be part of some document.
If every variable, ?V , in φ occurs in a subformulait is not physically part of the form Exists ...?V...(ψ) . Definition (Logical entailment). Let Γ be a RIF-BLD group orany document, it will be said to
belong to a special query document formula. If I is a
semantic multi-structure, Δ is the document of φ,
and IΔ is a component structure
in I, then TValI(φ an existentially closed) 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
condition formula.formulas. We say that Γ entails φ,
written as Γ |= φ, if and only if forevery
multi-structure I that is a model of Γ itis
the case that TVal I (also a model of φ ) = t. Equivalently, we can say ☐
Note that Γ |= φ holds iff whenever I |= Γ it followsone consequence of the multi-document semantics of
RIF-BLD is that also I |= φ . ☐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.
4 XML Serialization Syntax for
RIF-BLD
Editor's Note: TheRIF-BLD uses XML syntax, including the element tags, is being discussed by the Working Group. Input is welcome. See Issue-491.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.
4.1 XML for the RIF-BLD Condition
Language
XML serialization of the presentation syntax ofRIF-BLD in Section EBNF for RIF-BLD Condition
Language uses the following tags.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)
- arg (positional argumentargs (Atom/Expr positional arguments role, containing n TERMs)
- instance (Member instance role)
- upper (Member/Subclass upperclass (Member class role)
- lower (Member/Subclass lower instance/classsub (Subclass sub-class role)
- slot (Atom/Expr/Frame slot role, containing a Prop)super (Subclass super-class role)
- Prop (Property, prefix version ofslot infix '->') - key (Prop key(Atom/Expr or Frame slot role, containing a Const) - val (Prop val role, containingName 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><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.
Compact URI prefixes: bks expands into http://example.com/books# cpt expands into http://example.com/concepts# curr expands into http://example.com/currencies#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"^^rif:iri(?Buyer(cpt:purchase(?Buyer ?Seller
"cpt:book"^^rif:iri(?Author "bks:LeRif"^^rif:iri) "curr:USD"^^rif:iri("49"^^xsd:integer)))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> <arg><Var>Buyer</Var></arg> <arg><Var>Seller</Var></arg> <arg>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> <arg><Var>Author</Var></arg> <arg><Const type="rif:iri">bks:LeRif</Const></arg>type="&rif;iri">&cpt;book</Const></op>
<args rif:ordered="yes">
<Var>Author</Var>
<Const type="&rif;iri">&bks;LeRif</Const>
</args>
</Expr>
</arg> <arg><Expr>
<op><Const type="rif:iri">curr:USD</Const></op> <arg><Const type="xsd:integer">49</Const></arg>type="&rif;iri">&curr;USD</Const></op>
<args rif:ordered="yes"><Const type="&xsd;integer">49</Const></args>
</Expr>
</arg></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. Compact URI prefixes: bks expands into http://example.com/books# cpt expands into http://example.com/concepts# curr expands into http://example.com/currencies#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"^^rif:iri ?P["cpt:buyer"^^rif:iri->?Buyer "cpt:seller"^^rif:iri->?Seller "cpt:item"^^rif:iri->"cpt:book"^^rif:iri(cpt:author->?Author cpt:title->"bks:LeRif"^^rif:iri) "cpt:price"^^rif:iri->"49"^^xsd:integer "cpt:currency"^^rif:iri->"curr:USD"^^rif:iri]))(?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>
<lower><Var>P</Var></lower> <upper><Const type="rif:iri">cpt:purchase</Const></upper><instance><Var>P</Var></instance>
<class><Const type="&rif;iri">&cpt;purchase</Const></class>
</Member>
</formula>
<formula>
<Frame>
<object>
<Var>P</Var>
</object>
<slot> <Prop> <key><Const type="rif:iri">cpt:buyer</Const></key> <val><Var>Buyer</Var></val> </Prop><slot rif:ordered="yes">
<Const type="&rif;iri">&cpt;buyer</Const>
<Var>Buyer</Var>
</slot>
<slot> <Prop> <key><Const type="rif:iri">cpt:seller</Const></key> <val><Var>Seller</Var></val> </Prop><slot rif:ordered="yes">
<Const type="&rif;iri">&cpt;seller</Const>
<Var>Seller</Var>
</slot>
<slot> <Prop> <key><Const type="rif:iri">cpt:item</Const></key> <val><slot rif:ordered="yes">
<Const type="&rif;iri">&cpt;item</Const>
<Expr>
<op><Const type="rif:iri">cpt:book</Const></op> <slot> <Prop> <key><Name>cpt:author</Name></key> <val><Var>Author</Var></val> </Prop>type="&rif;iri">&cpt;book</Const></op>
<slot rif:ordered="yes">
<Name>&cpt;author</Name>
<Var>Author</Var>
</slot>
<slot> <Prop> <key><Name>cpt:title</Name></key> <val><Const type="rif:iri">bks:LeRif</Const></val> </Prop><slot rif:ordered="yes">
<Name>&cpt;title</Name>
<Const type="&rif;iri">&bks;LeRif</Const>
</slot>
</Expr>
</val> </Prop></slot>
<slot> <Prop> <key><Const type="rif:iri">cpt:price</Const></key> <val><Const type="xsd:integer">49</Const></val> </Prop><slot rif:ordered="yes">
<Const type="&rif;iri">&cpt;price</Const>
<Const type="&xsd;integer">49</Const>
</slot>
<slot> <Prop> <key><Const type="rif:iri">cpt:currency</Const></key> <val><Const type="rif:iri">curr:USD</Const></val> </Prop><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>
4.2 XML for the RIF-BLD Rule
Language
We now extend the RIF-BLD serialization from Section XML for RIF-BLD Condition
Language by including rulesrules, 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 optional payload annotated with metadata)payload)
- directive (directive role, containing Import)Import, Prefix, or Base)
- payload (payload role, containing Group)
- Import (importation, containing addresslocation and optional manner)profile)
- address (addresslocation (location role, containing Const of type iri)
- manner (mannerprofile (profile role, containing PROFILE)
- Group (nested collection of sentences annotated with metadata) - meta (meta role, containing metadata, which is represented as a Frame)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 groupdocument from Example
3. For convenience, the groupdocument is reproduced at the top and then
is followed by its serialization.
Compact URI prefixes: bks expands into http://example.com/books# auth expands into http://example.com/authors# cpt expands into http://example.com/concepts# dc expands into http://purl.org/dc/terms/ w3 expands into http://www.w3.org/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
" http://sample.org "^^rif:iri["dc:publisher"^^rif:iri->"w3:W3C"^^rif:iri "dc:date"^^rif:iri->"2008-04-04"^^xsd:date](
Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays (
"cpt:reject"^^rif:iri("ppl:John"^^rif:iricpt:reject(ppl:John ?item) :-
And("cpt:perishable"^^rif:iri(?item) "cpt:delivered"^^rif:iri(?itemAnd(cpt:perishable(?item)
cpt:delivered(?item ?deliverydate "ppl:John"^^rif:iri) "cpt:scheduled"^^rif:iri(?itemppl:John)
cpt:scheduled(?item ?scheduledate)
External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydateExternal(fn:subtract-dateTimes-yielding-dayTimeDuration(?deliverydate ?scheduledate ?diffduration))
External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffdurationExternal(fn:get-days-from-dayTimeDuration(?diffduration ?diffdays))
External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))External(op:numeric-greater-than(?diffdays 10)))
)
Forall ?item (
"cpt:reject"^^rif:iri("ppl:Fred"^^rif:iricpt:reject(ppl:Fred ?item) :- "cpt:unsolicited"^^rif:iri(?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:iri"> http://sample.org </Const>type="rif:local">pd</Const>
</object>
<slot> <Prop> <key><Const type="rif:iri">dc:publisher</Const></key> <val><Const type="rif:iri">w3:W3C</Const></val> </Prop><slot rif:ordered="yes">
<Const type="&rif;iri">&dc;publisher</Const>
<Const type="&rif;iri">&w3;W3C</Const>
</slot>
<slot> <Prop> <key><Const type="rif:iri">dc:date</Const></key> <val><Const type="xsd:date">2008-04-04</Const></val> </Prop><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> <arg><Var>item</Var></arg>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> <arg><Var>item</Var></arg> <arg><Var>deliverydate</Var></arg> <arg><Const type="rif:iri">ppl:John</Const></arg>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> <arg><Var>item</Var></arg> <arg><Var>scheduledate</Var></arg>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> <arg><Var>deliverydate</Var></arg> <arg><Var>scheduledate</Var></arg> <arg><Var>diffduration</Var></arg>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> <arg><Var>diffduration</Var></arg> <arg><Var>diffdays</Var></arg>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> <arg><Var>diffdays</Var></arg> <arg><Const type="xsd:long">10</Const></arg>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> <arg><Const type="rif:iri">ppl:John</Const></arg> <arg><Var>item</Var></arg>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> <arg><Var>item</Var></arg>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> <arg><Const type="rif:iri">ppl:Fred</Const></arg> <arg><Var>item</Var></arg>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>
4.3 Translation Between the RIF-BLD
Presentation and XML Syntaxes
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.
4.3.1 Translation of the RIF-BLD
Condition Language
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>
<arg><args rif:ordered="yes">
argument1'
</arg>. . .
<arg>argumentn'
</arg></args>
</Atom>
|
External (
atomicexpr
)
|
<External>
<content>atomicexpr'</content>
</External>
|
func (
argument1
. . .
argumentn
)
|
<Expr>
<op>func'</op>
<arg><args rif:ordered="yes">
argument1'
</arg>. . .
<arg>argumentn'
</arg></args>
</Expr>
|
pred (
unicodestring1 -> filler1
. . .
unicodestringn -> fillern
)
|
<Atom>
<op>pred'</op>
<slot> <Prop> <key><Name><slot rif:ordered="yes">
<Name>unicodestring1 </Name></key> <val></Name>
filler1'
</val> </Prop></slot>
. . .
<slot> <Prop> <key><Name><slot rif:ordered="yes">
<Name>unicodestringn </Name></key> <val></Name>
fillern'
</val> </Prop></slot>
</Atom>
|
func (
unicodestring1 -> filler1
. . .
unicodestringn -> fillern
)
|
<Expr>
<op>func'</op>
<slot> <Prop> <key><Name><slot rif:ordered="yes">
<Name>unicodestring1 </Name></key> <val></Name>
filler1'
</val> </Prop></slot>
. . .
<slot> <Prop> <key><Name><slot rif:ordered="yes">
<Name>unicodestringn </Name></key> <val></Name>
fillern'
</val> </Prop></slot>
</Expr>
|
inst [
key1 -> filler1
. . .
keyn -> fillern
]
|
<Frame>
<object>inst'</object>
<slot> <Prop> <key><slot rif:ordered="yes">
key1'
</key> <val>filler1'
</val> </Prop></slot>
. . .
<slot> <Prop> <key><slot rif:ordered="yes">
keyn'
</key> <val>fillern'
</val> </Prop></slot>
</Frame>
|
inst # class
|
<Member>
<lower><instance>inst' </lower> <upper></instance>
<class>class' </upper></class>
</Member>
|
sub ## super
|
<Subclass>
<lower><sub>sub' </lower> <upper></sub>
<super>super' </upper></super>
</Subclass>
|
left = right
|
<Equal>
<side>left'</side>
<side>right'</side>
</Equal>
|
unicodestring^^space
|
<Const type="space">unicodestring</Const>
|
?unicodestring
|
<Var>unicodestring</Var>
|
4.3.2 Translation of the RIF-BLD Rule
Language
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 |
Group ( clauseDocument(
Import(loc1)
. . .
clauseImport(locn)
<Group> <sentence> clausegroup
)
|
<Document>
<directive>
<Import>
<location>loc1' </sentence></location>
</Import>
</directive>
. . .
<sentence> clause<directive>
<Import>
<location>locn' </sentence> </Group></location>
</Import>
</directive>
<payload>group'</payload>
</Document>
|
Document(
Import(loc1 pro1)
. . .
Import(locn pron)
group
metaframe ()
|
<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>
<meta> metaframe' </meta><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>
|
5 Conformance Clauses
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
- it is a formula in the dialect D,
- all the data types used in φ are in Τ, and
- all the externally defined functions and predicates used in φ
are in Ε.
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.
6 RIF-BLD as a Specialization of the RIF
Framework
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.
5.16.1 The Presentation Syntax of RIF-BLD as
a Specialization of the Presentation Syntax of RIF-FLD
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.
- Alphabet.
-
The alphabet of the RIF-BLD
presentation syntax is the alphabet of RIF-FLD with the negation
symbols Neg and Naf excluded.
- Assignment of signatures to each constant and variable
symbol.
-
The signature set of RIF-BLD contains the following
signatures:
- Basic.
-
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.
- For every integer n ≥ 0, there are signatures
-
- fn{(individual ... individual) ⇒
individual} -- for n-ary function symbols,
- pn{(individual ... individual) ⇒ atomic} --
for n-ary predicates.
These represent function and predicate symbols of arity
n (each of the above cases has n
individuals as arguments inside the parentheses).
- For every set of symbols s1,...,sk ∈
ArgNames, there are signatures
fs1...sk{(s1->individual ... sk->individual) ⇒
individual} and ps1...sk{(s1->individual ...
sk->individual) ⇒ atomic}. These are signatures for terms
and predicates with arguments named s1, ..., sk,
respectively. In this specialization of RIF-FLD, the argument names
s1, ..., sk must be pairwise distinct.
- A symbol in Const can have exactly one signature,
individual, fn, or
pn, where n ≥ 0, or
fs1...sk{(s1->individual ... sk->individual) ⇒
individual}, ps1...sk{(s1->individual ...
sk->individual) ⇒ atomic}, for some
s1,...,sk ∈ ArgNames. It cannot have the
signature atomic, since only complex terms can have such
signatures. Thus, by itself a symbol cannot be a proposition in
RIF-BLD, but a term of the form p() can be.
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.
- The constant symbols that belong to the supported RIF data types
(XML Schema data types, rdf:XMLLiteral, rif:text)
all have the signature individual in RIF-BLD.
- The symbols of type rif:iri and rif:local can
have the following signatures in RIF-BLD: individual,
fn, or pn, for n =
0,1,....; or fs1...sk,
ps1...sk, for some argument names
s1,...,sk ∈ ArgNames.
- All variables are associated with signature
individual{ }, so they can range only over
individuals.
- The signature for equality is
={(individual individual) ⇒ atomic}.
This means that equality can compare only those terms whose
signature is individual; it cannot compare predicate names
or function symbols. Equality terms are also not allowed to occur
inside other terms, since the above signature implies that any term
of the form t = s has signature atomic and not
individual.
- The frame signature, ->, is
->{(individual individual individual) ⇒
atomic}.
Note that this precludes the possibility that a frame term might
occur as an argument to a predicate, a function, or inside some
other term.
- The membership signature, #, is
#{(individual individual) ⇒ atomic}.
Note that this precludes the possibility that a membership term
might occur as an argument to a predicate, a function, or inside
some other term.
- The signature for the subclass relationship is
##{(individual individual) ⇒ atomic}.
As with frames and membership terms, this precludes the
possibility that a subclass term might occur inside some other
term.
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.
- Supported types of terms.
-
- RIF-BLD supports all the term types defined by the syntactic
framework (see the Section Terms of RIF-FLD):
-
- constants
- variables
- positional
- with named arguments
- equality
- frame
- membership
- subclass
- external
- Compared to RIF-FLD, terms (both positional and with named
arguments) have significant restrictions. This is so in order to
give BLD a relatively compact nature.
-
- The signature for the variable symbols does not permit them to
occur in the context of predicates, functions, or formulas. In
particular, in the RIF-BLD specialization of RIF-FLD, a variable is
not an atomic formula.
- Likewise, a symbol cannot be an atomic formula by itself. That
is, if p ∈ Const then p is not a
well-formed atomic formula. However, p() can be an atomic
formula.
- Signatures permit only constant symbols to occur in the context
of function or predicate names. Indeed, RIF-BLD signatures ensure
that all variables have the signature individual{ }
and all other terms, except for the constants from Const,
can have either the signature individual{ } or
atomic{ }. Therefore, if t is a
(non-Const) term then t(...) is not a well-formed
term.
- In an externally defined term, External(t), t
can be only a positional, named-argument, or a frame term. Compared
to RIF-FLD, the above restricts t in that it cannot be a
constant.
- Supported symbol spaces.
-
RIF-BLD supports all the symbol spaces defined in Section
Constants and Symbol Spaces of the syntactic framework: xsd:string xsd:decimal xsd:time xsd:date xsd:dateTime rdf:XMLLiteral rif:text rif:iri rif:localdocument Data Types and
Built-Ins.
- Supported formulas.
-
RIF-BLD supports the following types of formulas (see Well-formed Terms
and Formulas for the definitions):
- RIF-BLD condition
-
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.
- RIF-BLD rule
-
A RIF-BLD rule is a universally quantified RIF-FLD rule with the
following restrictions:
- The head (or conclusion) of the rule is an atomic
formula, whichformula or a
conjunction of atomic formulas.
- None of the atomic formulas mentioned in the rule head is
notexternally defined (i.e., itcannot have the form
External(...)).
- The body (or premise) of the rule is a RIF-BLD condition.
- All free (non-quantified) variables in the rule must be
quantified with Forall outside of the rule (i.e.,
Forall ?vars (head :- body)).
- RIF-BLD group
A RIF-BLD group is a RIF-FLD group that contains only RIF-BLD
rules and RIF-BLD groups.
- RIF-BLD document
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.
Editor's Note: The list of supported symbol spaces will move to another document, Data Types and Built-Ins . Any existing discrepancies will be fixed at that time. 5.26.2 The Semantics of RIF-BLD as a
Specialization of RIF-FLD
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:
- The effect of the syntax.
-
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.
- Truth values.
-
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.
- Data types.
-
RIF-BLD supports all the data types listed in Section PrimitiveData Types of
RIF-FLD: xsd:long xsd:integer xsd:decimal xsd:string xsd:time xsd:dateTime rdf:XMLLiteral rif:textthe document Data Types
and Builtins.
- Logical entailment.
-
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:
- as a set of all models; or
- as the unique minimal model.
These two definitions are equivalent for entailment of
existentially closed RIF-BLD conditions by RIF-BLD setsdocuments (i.e.,
formulas where every variable, ?V, occurs in a subformula
of formulas,the form Exists ...?V...(ψ)), since all rules in
RIF-BLD are Horn -- it is a classical result of Van Emden and
Kowalski [vEK76].
Editor's Note: The list of supported data types will move to another document, Data Types and Built-Ins . Any existing discrepancies will be fixed at that time. 67 References
6.17.1 Normative References
- [RDF-CONCEPTS]
- 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]
- 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/.
- [RDF-SCHEMA]
- RDF Vocabulary Description Language 1.0: RDF Schema,
Brian McBride, Editor, W3C Recommendation 10 February 2004,
http://www.w3.org/TR/rdf-schema/.
- [RFC-3066]
- RFC 3066
- Tags for the Identification of Languages, H. Alvestrand,
IETF, January 2001. This document is http://www.isi.edu/in-notes/rfc3066.txt.
- [RFC-3987]
- RFC 3987
- Internationalized Resource Identifiers (IRIs), M. Duerst and
M. Suignard, IETF, January 2005. This document is http://www.ietf.org/rfc/rfc3987.txt.
- [XML-SCHEMA2]
- 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/.
6.27.2 Informational References
- [ANF01]
- Normal Form Conventions for XML Representations of
Structured Data, Henry S. Thompson. October 2001.
- [KLW95]
- Logical foundations of object-oriented and frame-based
languages, M. Kifer, G. Lausen, J. Wu. Journal of ACM, July
1995, pp. 741--843.
- [CKW93]
- 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.
- [CK95]
- 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.
- [RDFSYN04]
- 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/.
- [Shoham87]
- Nonmonotonic logics: meaning and utility, Y. Shoham.
Proc. 10th International Joint Conference on Artificial
Intelligence, Morgan Kaufmann, pp. 388--393, 1987.
- [CURIE]
- CURIE Syntax 1.0: A syntax for expressing Compact URIs,
Mark Birbeck, Shane McCarron. W3C Working Draft 2 April 2008.
Available at http://www.w3.org/TR/curie/.
- [GRS91]
- The Well-Founded Semantics for General Logic Programs,
A. Van Gelder, K.A. Ross, J.S. Schlipf. Journal of ACM, 38:3, pages
620-650, 1991.
- [GL88]
- The Stable Model Semantics for Logic Programming, M.
Gelfond and V. Lifschitz. Logic Programming: Proceedings of the
Fifth Conference and Symposium, pages 1070-1080, 1988.
- [vEK76]
- The semantics of predicate logic as a programming
language, M. van Emden and R. Kowalski. Journal of the ACM 23
(1976), 733-742.
78 Appendix: XML Schema for
RIF-BLD
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.
7.18.1 Condition Language
<?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>
7.28.2 Rule Language
<?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>