2.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 without reference to 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 we need to specialize for RIF-BLD.
Recall that the semantics of a dialect is derived
from these notions by specializing 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.
- Truth values.
-
The set TV of truth values in RIF-BLD consists of
just two values, t and f such that f
<t t. Clearly, <t is a total
order here.
- Data types.
-
RIF-BLD supports all the data types listed in Section Primitive Data
Types of RIF-FLD:
- xsd:long
- xsd:integer
- xsd:decimal
- xsd:string
- xsd:time
- xsd:dateTime
- rdf:XMLLiteral
- rif:text
- 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 RIF-BLD
conditions by RIF-BLD sets of formulas, since all rules in RIF-BLD
are Horn -- it is a classical result of Van Emden and Kowalski
[vEK76].
|
The list of supported data types will move to another document,
Data Types and
Built-Ins. Any existing discrepancies will be fixed at that
time.
|
3 Direct Specification of RIF-BLD
Syntax
This normative section specifies the syntax of RIF-BLD directly,
without referring to RIF-FLD. We define both a presentation
syntax and an XML syntax. The presentation syntax is not
intended to be a concrete syntax for RIF-BLD. It is defined in
Mathematical English and is intended to be used in the definitions
and examples. This syntax deliberately leaves out details such as
the delimiters of the various syntactic components, escape symbols,
parenthesizing, precedence of operators, and the like. Since RIF is
an interchange format, it uses XML as its concrete syntax.
3.1 Alphabet of RIF-BLD
Definition
(Alphabet). The alphabet 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 =, #, ##,
->, and External
- the grouping symbol Group
- auxiliary symbols, such as "(" and ")"
The set of connective symbols, quantifiers, =, etc., is
disjoint from Const and Var. The argument names
in ArgNames are written as unicode strings that must not
start with a question mark, "?". Variables are written as
Unicode strings preceded with the symbol "?".
Constants are written as "literal"^^symspace, where
literal is a sequence of Unicode characters and
symspace is an identifier for a symbol space. Symbol
spaces are defined in Section Symbol
Spaces of the RIF-FLD document.
|
The definition of symbol spaces will eventually be also given in
the document Data Types
and Builtins, so the above reference will be to that document
instead of 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).
The symbol Group is used to organize RIF-BLD rules into
collections and annotate them with metadata. ☐
The language of RIF-BLD is the set of formulas constructed using
the above alphabet according to the rules given below.
3.2 Terms
RIF-BLD supports several kinds of terms: constants and
variables, positional terms, terms with named
arguments, equality, membership, and
subclass atomic formulas, and frame formulas. The
word "term" will be used to refer to any kind of these
constructs.
Definition
(Term).
- Constants and variables. If t ∈ Const
or t ∈ Var then t is a simple
term.
- Positional terms. If t ∈ Const and
t1, ..., tn are
simple, positional, or named-argument 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 simple, positional, or
named-argument terms and s1, ...,
sn are pairwise distinct symbols from the set
ArgNames.
The term 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
simple, positional, or named-argument terms
then t = s is an equality
term.
- Class membership terms (or just membership
terms). t#s is a membership term if
t and s are simple, positional, or
named-argument terms.
- Subclass terms. t##s is a subclass
term if t and s are simple,
positional, or named-argument 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 simple, positional, or
named-argument terms.
- Externally defined terms. If t is a term then
External(t) is an externally defined
term.
-
Such terms are used for representing builtin functions and
predicates as well as "procedurally attached" terms or predicates,
which might exist in various rule-based systems, but are not
specified by RIF. ☐
Membership, subclass, and frame terms are used to describe
objects and class hierarchies.
3.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), which are allowed for
that symbol.
The arity of a symbol (or whether it is a predicate, a function,
or an individual) is not specified in RIF-BLD explicitly. Instead,
it is inferred as follows. Each constant symbol in a RIF-BLD
formula (or a set of formulas) may occur in at most one context: as
an individual, a function symbol of a particular arity, or a
predicate symbol of a particular arity. The arity of the symbol and
its type is then determined by its context. If a symbol from
Const occurs in more than one context in a set of
formulas, the set 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.
Also, if a term of the form External(p(...)) occurs as
an atomic formula then the occurrence of p is considered
to be a predicate occurrence.
|
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.
|
3.4 Formulas
Any term (positional or with named arguments) of the form
p(...) (or External(p(...)), where p is
a predicate symbol, is also an atomic formula.
Equality, membership, subclass, and frame terms are also atomic
formulas. A formula of the form External(p(...)) is also
called an externally defined atomic formula.
Simple terms (constants and variables) are not formulas.
Not all atomic formulas are 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.
- Conjunction: If φ1, ...,
φn, n ≥ 0, are well-formed 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 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 formula and
?V1, ..., ?Vn are variables
then Exists ?V1 ... ?Vn(φ)
is an existential formula.
Formulas constructed using the above definitions are called
RIF-BLD
conditions. The following formulas lead to the
notion of a RIF-BLD rule.
- Rule implication: If φ is an well-formed atomic
formula and ψ is a RIF-BLD condition then φ :-
ψ is a well-formed formula, called rule implication,
provided that φ is not externally defined (i.e.,
does not have the form External(...)).
- Quantified rule: If φ is a rule implication and
?V1, ..., ?Vn are variables
then Forall ?V1 ... ?Vn(φ)
is a well-formed formula, called quantified rule. It is
required that all the free (i.e., non-quantified) variables in
φ occur in the prefix Forall ?V1
... ?Vn. Quantified rules will also be
referred to as RIF-BLD rules.
- Group: If φ is a frame term and
ρ1, ..., ρn are RIF-BLD
rules or group formulas (they can be mixed) then Group φ
(ρ1 ... ρn) and Group (ρ1
... ρn) are group formulas.
Group formulas are intended to represent sets of rules annotated
with metadata. This metadata is specified using an optional frame
term φ. Note that some of the ρi's can
be group formulas themselves, which means that groups can be
nested. This allows one to attach metadata to various subsets of
rules, which may be inside larger rule sets, which in turn can be
annotated. ☐
It can be seen from the definitions that RIF-BLD has a wide
variety of syntactic forms for terms and formulas. This provides
the infrastructure for exchanging rule languages that support rich
collections of syntactic forms. Systems that do not support some of
that 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).
3.5 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
does not 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: it does not
address the details of how constants and variables are represented,
and it is not sufficiently precise about the delimiters and escape
symbols. Instead, white space is informally used as a delimiter,
and white space is implied in productions that use Kleene star. For
instance, TERM* is to be understood as
TERM TERM ... TERM, where each ' '
abstracts from one or more blanks, tabs, newlines, etc. This is
done on intentionally, since RIF's presentation syntax is intended
as a tool for specifying the semantics and for illustration of the
main RIF concepts through examples. It is not intended as a
concrete syntax for a rule language. RIF defines a concrete syntax
only for exchanging rules, and that syntax is XML-based,
obtained as a refinement and serialization of the EBNF syntax.
- For all the above reasons, the EBNF syntax is not
normative.
3.5.1 EBNF for RIF-BLD Condition
Language
The Condition Language represents formulas that can be used in
the body of the RIF-BLD rules. It is intended to be a common part
of a number of RIF dialects, including RIF PRD. The EBNF grammar
for a superset of the RIF-BLD condition language is as follows.
FORMULA ::= 'And' '(' FORMULA* ')' |
'Or' '(' FORMULA* ')' |
'Exists' Var+ '(' FORMULA ')' |
ATOMIC |
'External' '(' Atom ')'
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
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, but RIF-FLD
Syntax allows arbitrary quantification, which can be used in
some dialects. 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 except for using Unicode strings in constant
symbols, as names, and for variables. Constant symbols have the
form: "UNICODESTRING"^^SYMSPACE, where SYMSPACE
is an IRI string that identifies the symbol space of the constant
and UNICODESTRING is a Unicode string from the lexical
space of that symbol space. Names are just denoted by Unicode
character sequences. Variables are denoted by Unicode character
sequences beginning 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 of
RIF-DTB. Likewise,
an External Expr is a call to an externally
defined function of RIF-DTB.
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, or
property values. For brevity, we use the compact URI
notation [CURIE],
prefix:suffix, which should be understood as a macro that
expands into a concatenation of the prefix definition and
suffix. Thus, if bks is a prefix that expands
into http://example.com/books# then bks:LeRif
should be understood merely as an abbreviation for
http://example.com/books#LeRif. The compact URI notation
is not part of the 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#
Positional terms:
"cpt:book"^^rif:iri("auth:rifwg"^^rif:iri "bks:LeRif"^^rif:iri)
Exists ?X ("cpt:book"^^rif:iri(?X "bks:LeRif"^^rif:iri))
Terms with named arguments:
"cpt:book"^^rif:iri(cpt:author->"auth:rifwg"^^rif:iri
cpt:title->"bks:LeRif"^^rif:iri)
Exists ?X ("cpt:book"^^rif:iri(cpt:author->?X cpt:title->"bks:LeRif"^^rif:iri))
Frames:
"bks:wd1"^^rif:iri["cpt:author"^^rif:iri->"auth:rifwg"^^rif:iri
"cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri]
Exists ?X ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->?X
"cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri])
Exists ?X ("bks:wd2"^^rif:iri # "cpt:book"^^rif:iri["cpt:author"^^rif:iri->?X
"cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri])
Exists ?I ?X (?I["cpt:author"^^rif:iri->?X "cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri])
Exists ?I ?X (?I # "cpt:book"^^rif:iri["cpt:author"^^rif:iri->?X
"cpt:title"^^rif:iri->"bks:LeRif"^^rif:iri])
Exists ?S ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->"auth:rifwg"^^rif:iri
?S->"bks:LeRif"^^rif:iri])
Exists ?X ?S ("bks:wd2"^^rif:iri["cpt:author"^^rif:iri->?X
?S->"bks:LeRif"^^rif:iri])
Exists ?I ?X ?S (?I # "cpt:book"^^rif:iri[author->?X ?S->"bks:LeRif"^^rif:iri])
3.5.2 EBNF for RIF-BLD Rule
Language
The presentation syntax for Horn rules extends the syntax in
Section EBNF for
RIF-BLD Condition Language with the following productions.
Group ::= 'Group' IRIMETA? '(' (RULE | Group)* ')'
IRIMETA ::= Frame
RULE ::= 'Forall' Var+ '(' CLAUSE ')' | CLAUSE
CLAUSE ::= Implies | ATOMIC
Implies ::= ATOMIC ':-' FORMULA
For convenient reference, we reproduce the condition language
part of the EBNF below.
FORMULA ::= 'And' '(' FORMULA* ')' |
'Or' '(' FORMULA* ')' |
'Exists' Var+ '(' FORMULA ')' |
ATOMIC |
'External' '(' Atom ')'
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
A RIF-BLD Group is a nested collection of RIF-BLD rules
annotated with optional metadata, IRIMETA, represented as
Frames. A Group can contain any number of
RULEs along with any number of nested Groups.
Rules are generated by CLAUSE, which can be in the scope
of a Forall quantifier. If a CLAUSE in the
RULE production has a free (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 into the yet-to-be-determined IRI for RIF builtin predicates
a. Universal form:
Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays (
"cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item) :-
And("cpt:perishable"^^rif:iri(?item)
"cpt:delivered"^^rif:iri(?item ?deliverydate "ppl:John"^^rif:iri)
"cpt:scheduled"^^rif:iri(?item ?scheduledate)
External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration))
External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffduration ?diffdays))
External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))
)
b. Universal-existential form:
Forall ?item (
"cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item ) :-
Exists ?deliverydate ?scheduledate ?diffduration ?diffdays (
And("cpt:perishable"^^rif:iri(?item)
"cpt:delivered"^^rif:iri(?item ?deliverydate "ppl:John"^^rif:iri)
"cpt:scheduled"^^rif:iri(?item ?scheduledate)
External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration))
External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffduration ?diffdays))
External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))
)
)
Example 3 (A RIF-BLD group annotated with metadata).
This example shows 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 Dublin Core metadata represented as a
frame.
Compact URI prefixes:
bks expands into http://example.com/books#
auth expands into http://example.com/authors#
cpt expands into http://example.com/concepts#
dc expands into http://dublincore.org/documents/dces/
w3 expands into http://www.w3.org/
Group "http://sample.org"^^rif:iri["dc:publisher"^^rif:iri->"w3:W3C"^^rif:iri
"dc:date"^^rif:iri->"2008-04-04"^^xsd:date]
(
Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays (
"cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item) :-
And("cpt:perishable"^^rif:iri(?item)
"cpt:delivered"^^rif:iri(?item ?deliverydate "ppl:John"^^rif:iri)
"cpt:scheduled"^^rif:iri(?item ?scheduledate)
External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration))
External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffduration ?diffdays))
External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))
)
Forall ?item (
"cpt:reject"^^rif:iri("ppl:Fred"^^rif:iri ?item) :- "cpt:unsolicited"^^rif:iri(?item)
)
)
4 Direct Specification of RIF-BLD
Semantics
This normative section specifies the semantics of RIF-BLD
directly, without referring to RIF-FLD.
4.1 Truth Values
The set TV of truth values in RIF-BLD consists of
just two values, t and f.
4.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 that denote function symbols. As before,
Const denotes the set of all constant symbols and
Var the set of all variable symbols. TV
denotes the set of truth values that the semantic structure uses
and DTS is the set of primitive data types used in
I (please refer to Section Primitive Data
Types of RIF-FLD for the semantics of data types).
The other components of I are total mappings
defined as follows:
- I C maps Const to
D.
This mapping interprets constant symbols. In addition:
-
- If a constant, c ∈ Const, denotes
an individual then it is required that
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 object then the result is also an individual
object.
- ISF is a total mapping from
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 is a total mapping from
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 ?A->?B] becomes
o[a->b a->b] if variable ?A is
instantiated with the symbol a and ?B with
b.
- Isub gives meaning to the subclass
relationship. It is a total function 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 total function 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 total function
Dind × Dind →
D.
It gives meaning to the equality operator.
- Itruth is a total mapping
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
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). Then the following must hold:
- VSdt ⊆ Dind;
and
- For each constant "lit"^^dt ∈
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.
☐
4.3 Interpretation of
Formulas
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 different attribute/value pairs are supposed to be
understood as conjunctions, 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 (ρ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 of rules, Γ, is a
semantic structure I such that
TValI(Γ) = 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.
4.4 Logical Entailment
We now define what it means for a set of RIF-BLD rules to entail
a RIF-BLD condition. We say that a RIF-BLD condition formula
φ is existentially closed, if and only if every
variable, ?V, in φ occurs in a subformula of the
form Exists ...?V...(ψ).
Definition
(Logical entailment). Let Γ be a RIF-BLD group formula
and φ an existentially closed RIF-BLD condition formula.
We say that Γ entails φ, written as
Γ |= φ, if and only if for every model of
Γ it is the case that TValI(φ)
= t.
Equivalently, we can say that Γ |= φ holds
iff whenever I |= Γ it
follows that also I |= φ.
☐
5 XML Serialization Syntax for
RIF-BLD
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.
5.1 XML for RIF-BLD Condition
Language
XML serialization of the presentation syntax of Section EBNF for RIF-BLD Condition
Language uses the following tags.
- And (conjunction)
- Or (disjunction)
- Exists (quantified formula for 'Exists', containing declare and formula roles)
- declare (declare role, containing a Var)
- formula (formula role, containing a FORMULA)
- Atom (atom formula, positional or with named arguments)
- External (external call, containing a content role)
- content (content role, containing an Atom, for predicates, or Expr, for functions)
- Member (member formula)
- Subclass (subclass formula)
- Frame (Frame formula)
- object (Member/Frame role, containing a TERM or an object description)
- op (Atom/Expr role for predicates/functions as operations)
- arg (positional argument role)
- upper (Member/Subclass upper class role)
- lower (Member/Subclass lower instance/class role)
- slot (Atom/Expr/Frame slot role, containing a Prop)
- Prop (Property, prefix version of slot infix '->')
- key (Prop key role, containing a Const)
- val (Prop val role, containing a TERM)
- Equal (prefix version of term equation '=')
- Expr (expression formula, positional or with named arguments)
- side (Equal 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>.
Example 4 (A RIF condition and its XML serialization).
This example illustrates XML serialization for RIF conditions.
As before, the compact URI notation is used for better
readability.
Compact URI prefixes:
bks expands into http://example.com/books#
cpt expands into http://example.com/concepts#
curr expands into http://example.com/currencies#
RIF condition
And (Exists ?Buyer ("cpt:purchase"^^rif:iri(?Buyer
?Seller
"cpt:book"^^rif:iri(?Author "bks:LeRif"^^rif:iri)
"curr:USD"^^rif:iri("49"^^xsd:integer)))
?Seller=?Author )
XML serialization
<And>
<formula>
<Exists>
<declare><Var>Buyer</Var></declare>
<formula>
<Atom>
<op><Const type="rif:iri">cpt:purchase</Const></op>
<arg><Var>Buyer</Var></arg>
<arg><Var>Seller</Var></arg>
<arg>
<Expr>
<op><Const type="rif:iri">cpt:book</Const></op>
<arg><Var>Author</Var></arg>
<arg><Const type="rif:iri">bks:LeRif</Const></arg>
</Expr>
</arg>
<arg>
<Expr>
<op><Const type="rif:iri">curr:USD</Const></op>
<arg><Const type="xsd:integer">49</Const></arg>
</Expr>
</arg>
</Atom>
</formula>
</Exists>
</formula>
<formula>
<Equal>
<side><Var>Seller</Var></side>
<side><Var>Author</Var></side>
</Equal>
</formula>
</And>
Example 5 (A RIF condition and its XML serialization).
This example illustrates XML serialization of RIF conditions
that involve terms with named arguments.
Compact URI prefixes:
bks expands into http://example.com/books#
auth expands into http://example.com/authors#
cpt expands into http://example.com/concepts#
curr expands into http://example.com/currencies#
RIF condition:
And (Exists ?Buyer ?P (
?P#"cpt:purchase"^^rif:iri["cpt:buyer"^^rif:iri->?Buyer
"cpt:seller"^^rif:iri->?Seller
"cpt:item"^^rif:iri->"cpt:book"^^rif:iri(cpt:author->?Author
cpt:title->"bks:LeRif"^^rif:iri)
"cpt:price"^^rif:iri->"49"^^xsd:integer
"cpt:currency"^^rif:iri->"curr:USD"^^rif:iri])
?Seller=?Author)
XML serialization:
<And>
<formula>
<Exists>
<declare><Var>Buyer</Var></declare>
<declare><Var>P</Var></declare>
<formula>
<Frame>
<object>
<Member>
<lower><Var>P</Var></lower>
<upper><Const type="rif:iri">cpt:purchase</Const></upper>
</Member>
</object>
<slot>
<Prop>
<key><Const type="rif:iri">cpt:buyer</Const></key>
<val><Var>Buyer</Var></val>
</Prop>
</slot>
<slot>
<Prop>
<key><Const type="rif:iri">cpt:seller</Const></key>
<val><Var>Seller</Var></val>
</Prop>
</slot>
<slot>
<Prop>
<key><Const type="rif:iri">cpt:item</Const></key>
<val>
<Expr>
<op><Const type="rif:iri">cpt:book</Const></op>
<slot>
<Prop>
<key><Name>cpt:author</Name></key>
<val><Var>Author</Var></val>
</Prop>
</slot>
<slot>
<Prop>
<key><Name>cpt:title</Name></key>
<val><Const type="rif:iri">bks:LeRif</Const></val>
</Prop>
</slot>
</Expr>
</val>
</Prop>
</slot>
<slot>
<Prop>
<key><Const type="rif:iri">cpt:price</Const></key>
<val><Const type="xsd:integer">49</Const></val>
</Prop>
</slot>
<slot>
<Prop>
<key><Const type="rif:iri">cpt:currency</Const></key>
<val><Const type="rif:iri">curr:USD</Const></val>
</Prop>
</slot>
</Frame>
</formula>
</Exists>
</formula>
<formula>
<Equal>
<side><Var>Seller</Var></side>
<side><Var>Author</Var></side>
</Equal>
</formula>
</And>
5.2 XML for RIF-BLD Rule
Language
We now extend the RIF-BLD serialization from Section XML for RIF-BLD Condition
Language by including rules as described in Section EBNF for RIF-BLD Rule
Language. The extended serialization uses the following
additional tags.
- Group (nested collection of rules annotated with metadata)
- meta (meta role, containing metadata, which is represented as a Frame)
- rule (rule role, containing RULE)
- Forall (quantified formula for 'Forall', containing declare and formula roles)
- Implies (implication, containing if and then roles)
- if (antecedent role, containing FORMULA)
- then (consequent role, containing ATOMIC)
The XML Schema Definition of RIF-BLD is given in Appendix
XML Schema for BLD.
Example 6 (Serializing a RIF-BLD group annotated with
metadata).
This example shows a serialization for the group from Example 3.
For convenience, the group is reproduced at the top and then is
followed by its serialization.
Compact URI prefixes:
bks expands into http://example.com/books#
auth expands into http://example.com/authors#
cpt expands into http://example.com/concepts#
dc expands into http://dublincore.org/documents/dces/
w3 expands into http://www.w3.org/
Presentation syntax:
Group "http://sample.org"^^rif:iri["dc:publisher"^^rif:iri->"w3:W3C"^^rif:iri
"dc:date"^^rif:iri->"2008-04-04"^^xsd:date]
(
Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays (
"cpt:reject"^^rif:iri("ppl:John"^^rif:iri ?item) :-
And("cpt:perishable"^^rif:iri(?item)
"cpt:delivered"^^rif:iri(?item ?deliverydate "ppl:John"^^rif:iri)
"cpt:scheduled"^^rif:iri(?item ?scheduledate)
External("fn:subtract-dateTimes-yielding-dayTimeDuration"^^rif:iri(?deliverydate ?scheduledate ?diffduration))
External("fn:get-days-from-dayTimeDuration"^^rif:iri(?diffduration ?diffdays))
External("op:numeric-greater-than"^^rif:iri(?diffdays "10"^^xsd:integer)))
)
Forall ?item (
"cpt:reject"^^rif:iri("ppl:Fred"^^rif:iri ?item) :- "cpt:unsolicited"^^rif:iri(?item)
)
)
XML syntax:
<Group>
<meta>
<Frame>
<object>
<Const type="rif:iri">http://sample.org</Const>
</object>
<slot>
<Prop>
<key><Const type="rif:iri">dc:publisher</Const></key>
<val><Const type="rif:iri">w3:W3C</Const></val>
</Prop>
</slot>
<slot>
<Prop>
<key><Const type="rif:iri">dc:date</Const></key>
<val><Const type="xsd:date">2008-04-04</Const></val>
</Prop>
</slot>
</Frame>
</meta>
<rule>
<Forall>
<declare><Var>item</Var></declare>
<declare><Var>deliverydate</Var></declare>
<declare><Var>scheduledate</Var></declare>
<declare><Var>diffduration</Var></declare>
<declare><Var>diffdays</Var></declare>
<formula>
<Implies>
<if>
<And>
<formula>
<Atom>
<op><Const type="rif:iri">cpt:perishable</Const></op>
<arg><Var>item</Var></arg>
</Atom>
</formula>
<formula>
<Atom>
<op><Const type="rif:iri">cpt:delivered</Const></op>
<arg><Var>item</Var></arg>
<arg><Var>deliverydate</Var></arg>
<arg><Const type="rif:iri">ppl:John</Const></arg>
</Atom>
</formula>
<formula>
<Atom>
<op><Const type="rif:iri">cpt:scheduled</Const></op>
<arg><Var>item</Var></arg>
<arg><Var>scheduledate</Var></arg>
</Atom>
</formula>
<formula>
<External>
<content>
<Atom>
<op><Const type="rif:iri">fn:subtract-dateTimes-yielding-dayTimeDuration</Const></op>
<arg><Var>deliverydate</Var></arg>
<arg><Var>scheduledate</Var></arg>
<arg><Var>diffduration</Var></arg>
</Atom>
</content>
</External>
</formula>
<formula>
<External>
<content>
<Atom>
<op><Const type="rif:iri">fn:get-days-from-dayTimeDuration</Const></op>
<arg><Var>diffduration</Var></arg>
<arg><Var>diffdays</Var></arg>
</Atom>
</content>
</External>
</formula>
<formula>
<External>
<content>
<Atom>
<op><Const type="rif:iri">op:numeric-greater-than</Const></op>
<arg><Var>diffdays</Var></arg>
<arg><Const type="xsd:long">10</Const></arg>
</Atom>
</content>
</External>
</formula>
</And>
</if>
<then>
<Atom>
<op><Const type="xsd:long">reject</Const></op>
<arg><Const type="rif:iri">ppl:John</Const></arg>
<arg><Var>item</Var></arg>
</Atom>
</then>
</Implies>
</formula>
</Forall>
</rule>
<rule>
<Forall>
<declare><Var>item</Var></declare>
<formula>
<Implies>
<if>
<Atom>
<op><Const type="rif:iri">cpt:unsolicited</Const></op>
<arg><Var>item</Var></arg>
</Atom>
</if>
<then>
<Atom>
<op><Const type="rif:iri">cpt:reject</Const></op>
<arg><Const type="rif:iri">ppl:Fred</Const></arg>
<arg><Var>item</Var></arg>
</Atom>
</then>
</Implies>
</formula>
</Forall>
</rule>
</Group>
5.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.
5.3.1 Translation of 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>argument1'</arg>
. . .
<arg> argumentn'</arg>
</Atom>
|
External (
atomexpr
)
|
<External>
<content>atomexpr'</content>
</External>
|
func (
argument1
. . .
argumentn
)
|
<Expr>
<op>func'</op>
<arg>argument1'</arg>
. . .
<arg> argumentn'</arg>
</Expr>
|
pred (
unicode1 -> filler1
. . .
unicoden -> fillern
)
|
<Atom>
<op>pred'</op>
<slot>
<Prop>
<key><Name>unicode1</Name></key>
<val>filler1'</val>
</Prop>
</slot>
. . .
<slot>
<Prop>
<key><Name>unicoden</Name></key>
<val>fillern'</val>
</Prop>
</slot>
</Atom>
|
func (
unicode1 -> filler1
. . .
unicoden -> fillern
)
|
<Expr>
<op>func'</op>
<slot>
<Prop>
<key><Name>unicode1</Name></key>
<val>filler1'</val>
</Prop>
</slot>
. . .
<slot>
<Prop>
<key><Name>unicoden</Name></key>
<val>fillern'</val>
</Prop>
</slot>
</Expr>
|
inst [
key1 -> filler1
. . .
keyn -> fillern
]
|
<Frame>
<object>inst'</object>
<slot>
<Prop>
<key>key1'</key>
<val>filler1'</val>
</Prop>
</slot>
. . .
<slot>
<Prop>
<key>keyn'</key>
<val>fillern'</val>
</Prop>
</slot>
</Frame>
|
inst # class [
key1 -> filler1
. . .
keyn -> fillern
]
|
<Frame>
<object>
<Member>
<lower>inst'</lower>
<upper>class'</upper>
</Member>
</object>
<slot>
<Prop>
<key>key1'</key>
<val>filler1'</val>
</Prop>
</slot>
. . .
<slot>
<Prop>
<key>keyn'</key>
<val>fillern'</val>
</Prop>
</slot>
</Frame>
|
sub ## super [
key1 -> filler1
. . .
keyn -> fillern
]
|
<Frame>
<object>
<Subclass>
<lower>sub'</lower>
<upper>super'</upper>
</Subclass>
</object>
<slot>
<Prop>
<key>key1'</key>
<val>filler1'</val>
</Prop>
</slot>
. . .
<slot>
<Prop>
<key>keyn'</key>
<val>fillern'</val>
</Prop>
</slot>
</Frame>
|
inst # class
|
<Member>
<lower>inst'</lower>
<upper>class'</upper>
</Member>
|
sub ## super
|
<Subclass>
<lower>sub'</lower>
<upper>super'</upper>
</Subclass>
|
left = right
|
<Equal>
<side>left'</side>
<side>right'</side>
</Equal>
|
unicode^^space
|
<Const type="space">unicode</Const>
|
?unicode
|
<Var>unicode</Var>
|
5.3.2 Translation of 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 (
clause1
. . .
clausen
)
|
<Group>
<rule>clause1'</rule>
. . .
<rule>clausen'</rule>
</Group>
|
Group metaframe (
clause1
. . .
clausen
)
|
<Group>
<meta>metaframe'</meta>
<rule>clause1'</rule>
. . .
<rule>clausen'</rule>
</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>
|