2.2 Alphabet of RIF-BLDThe alphabetSemantics of RIF-BLD consists of a countably infinite set of constant symbols Const , a countably infinite set of variable symbols Var (disjoint from Const ),as a countably infinite setSpecialization of argument names, ArgNames (disjoint from Const and Var ), connective symbols And and Or , quantifiers Exists and Forall ,RIF-FLD
This normative section defines the symbols = , # , ## , -> , :- , and auxiliary symbols, such as "(" and ")".precise relationship between the setsemantics of connective symbols, quantifiers, = , etc., is disjoint from ConstRIF-BLD and Var . Variables are written as Unicode strings preceded withthe symbol "?".semantic framework of RIF-FLD. Specification of the syntax for constant symbolssemantics without reference to RIF-FLD is given in Section Symbol SpacesDirect Specification of RIF-FLD.RIF-BLD Semantics.
The languagesemantics of RIF-BLDthe RIF Basic Logic Dialect is defined by specialization from the setsemantics of formulas constructed using the above alphabet according tothe rules spelled out below. 2.3 Terms RIF-BLD supports several kindsSemantic Framework for Logic Dialects of RIF. Section Semantics of a RIF Dialect as a Specialization of terms: constants and variables , positional terms, terms with named arguments , equality , membership , and subclass terms, and frames .the word " term " will be used to referRIF Framework in that document lists the parameters of the semantic framework, which we need to any kindspecialize for RIF-BLD.
Recall that the semantics of terms. Formally, terms are defined as follows: Constants and variables . If t ∈ Const or t ∈ Var then t isa simple termdialect is derived from these notions by specializing the following parameters.
- The effect of the syntax.
Positional termsRIF-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.
IfThe set TV of truth values in RIF-BLD consists of just two values, t ∈ Constand f such that f <t 1 , ...,t n are terms then t(t 1 .... Clearly, <t n )is a positional termtotal order here.
- Data types.
Terms with named argumentsRIF-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.
A term with named arguments (a termRecall that logical entailment in RIF-FLD is defined with named arguments)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 form t(s 1 ->v 1 ... s n ->v n ) , where t ∈ Const , v 1 , ..., v ntwo following equivalent ways:
- as a set of all models; or
- as the unique minimal model.
These two definitions are terms (positional, with named arguments, frame, etc.), and s 1 , ..., s nequivalent for entailment of RIF-BLD conditions by RIF-BLD sets of formulas, since all rules in RIF-BLD are (not necessarily distinct) symbols fromHorn -- it is a classical result of Van Emden and Kowalski [vEK76].
|
The set ArgNameslist 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 term t here represents a predicate orsyntax of RIF-BLD directly, without referring to RIF-FLD. We define both a function; s 1 , ..., s n represent argument names;presentation syntax and v 1 , ..., v n represent argument values. Terms with named arguments are like positional terms except thatan XML syntax. The arguments are named and their orderpresentation syntax is immaterial. Note thatnot intended to be a term like f()concrete syntax for RIF-BLD. It is both positionaldefined in Mathematical English and with named arguments. Equality terms . If tis intended to be used in the definitions and s are terms then t = sexamples. 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 equality terminterchange format, it uses XML as its concrete syntax.
3.1 Alphabet of RIF-BLD
Definition (Alphabet).
Class membership terms (or just membership terms ). t#s isThe alphabet of RIF-BLD consists of
- a
membership term if t and s are arbitrary terms. Subclass terms . t##s is a subclass term if t and s are arbitrary terms. Frame terms . t[p 1 ->v 1 ... p n ->v n ] iscountably infinite set of constant symbols Const
- a
frame term (or simplycountably infinite set of variable symbols Var (disjoint from Const)
- a
framecountably infinite set of argument names, ArgNames (disjoint from Const and Var)
-
if tconnective symbols And, p 1Or, ..., p nand :-
- quantifiers Exists and Forall
- the symbols =,
v 1#, ..., v n##, ->, n ≥ 0, are arbitrary terms. Membership, subclass,and frame terms are used to describe objects in object-based logics like F-logic [ KLW95 ]. These terms can be readily mixed both with positional termsExternal
- the grouping symbol Group
- auxiliary symbols, such as "(" and
terms with named arguments: p(?X q#r[v(1,2)->s] t(d->e f->g)) . 2.4 Well-formedness")"
The set of allconnective symbols, Constquantifiers, =, etc., is partitioned into positional predicate symbols, predicate symbols with named arguments, positional function symbols, function symbols with named arguments, and individuals. Each positional predicatedisjoint from Const and function symbol has precisely one arity , which is a non-negative integer that tells how many argumentsVar. The symbol can take. An arity for terms with named arguments (of a symbol with named arguments) is a bag {s 1 ... s k } ofargument names ( s i ∈in ArgNames ). Each predicate or function symbolare written as unicode strings that must not start with named arguments has precisely one arity (for termsa question mark, "?". Variables are written as Unicode strings preceded with named arguments).the arity of asymbol (or whether it"?".
Constants are written as "literal"^^symspace, where literal is a predicate, a function, or an individual) is not specified explicitly in RIF-BLD. Instead, it is inferred as follows. Each constant symbol in a RIF-BLD formula (or a setsequence of formulas)Unicode characters and
symspace is expected to occur in at most one context: asan individual,identifier for a functionsymbol of a particular arity, a predicatespace. Symbol spaces are defined in Section Symbol Spaces of a particular arity, or an individual.the arity ofRIF-FLD document.
|
The definition of symbol and its type is then determined by its context. If a symbol from Const occursspaces will eventually be also given in more than one context,the
formula (or a set of formulas) is not considered todocument Data Types and Builtins, so the above reference will be well-formed in RIF-BLD. 2.5 Formulas Any term (positional or with named arguments)to
that document instead of RIF-FLD.
|
The form p(...)symbols =, where p is a predicate symbol, is also an atomic formula .#, and ## are used in formulas that define equality, class membership, subclass,and frame terms are also atomic formula. Simplesubclass relationships. The symbol -> is used in terms (constantsthat have named arguments and variables) are notin frame formulas. Not all atomic formulas are well-formed -- see Section Well-formedness . A well-formed atomic formula isThe symbol External indicates that an atomic formula thator a function term is alsodefined externally (e.g., a well-formed term. More general formulas are constructed out ofbuiltin).
The atomic formulassymbol Group is used to organize RIF-BLD rules into collections and annotate them with metadata. ☐
The helplanguage of logical connectives. A formulaRIF-BLD is a statement that can have onethe set of formulas constructed using the following forms: Atomic : If φ is a well-formed atomic formulaabove 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
itt is alsoa formula. Conjunction :simple term.
- Positional terms. If
φt Const and t1, ..., φ n ,tn ≥ 0,are formulassimple, positional, or named-argument terms then so is And( φt(t1 ... φtn) . As a special case, And()is allowed and is treated asa tautology, i.e.,positional term.
- Terms with named arguments. A
formula thatterm with named arguments is always true. Disjunction : If φof the form t(s1 , ..., φ n , n ≥ 0, are formulas then so is Or( φ->v1 ... φsn->vn) . When n=0, we get Or() as a special case; it is treated as a formula that is always false. Existentials : If φ is a formulawhere t Const and ?Vv1, ..., ?Vvn are variables then Exists ?Vsimple, positional, or named-argument terms and s1 ... ?V, ..., sn ( φ ) is a formula. Formulas constructed using the above definitionsare called RIF-BLD conditionspairwise distinct symbols from the set ArgNames.
RIF-BLD rules are defined as follows: Rule : If φ is an atomic formula and ψ is a RIF-BLD condition then φ :- ψ is a formula, provided that φ does not haveThe signature bi_atomic (i.e., is notterm t here represents a builtin predicate). Universals : If φ ispredicate or a rule and ?Vfunction; s1, ..., ?Vsn are variables then Forall ?Vrepresent argument names; and v1 ... ?V, ..., vn ( φ ) is a formula, called an explicitly quantified rule . 2.6 EBNF Grammar for the Presentation Syntax of RIF-BLD So far, the syntax of RIF-BLD was specified in Mathematical English. Tool developers, however, preferrepresent argument values. The more formal EBNF notation, which we will give next. Several points shouldargument names, s1, ..., sn, are required to be kept in mind regarding this notation.pairwise distinct. Terms with named arguments are like positional terms except that the syntax of first-order logicarguments are named and their order is not context-free, so EBNF cannot capture the syntax of RIF-BLD precisely. For instance, it cannot capture the well-formedness conditions , i.e., the requirementimmaterial. Note that each symbol in RIF-BLD can occur in at most one context. As a result, the grammar, below, defines onlya supersetterm of RIF-BLD.the EBNF syntaxform f() is not a concrete syntax: it does not address the details of how constantsboth positional and variables are represented,with named arguments.
- Equality terms. If t and
its are simple, positional, or named-argument terms then t=s is not sufficiently precise about the delimiters and escape symbols. Instead, white spacean equality term.
- Class membership terms (or just membership terms). t#s is
informally used asa delimiter,membership term if t and white space is implied in productions that use Kleene star. For instance, TERM* is to be understood as TERM TERM ... TERMs are simple, positional, where each ' ' abstracts from oneor more blanks, tabs, newlines, etc. This is done on purpose, since RIF's presentation syntaxnamed-argument terms.
- Subclass terms. t##s is
intended asa tool for specifying the semanticssubclass term if t and for illustration of the main RIF concepts through examples. Its are simple, positional, or named-argument terms.
- Frame terms. t[p1->v1 ... pn->vn] is
not intended asa concrete syntax forframe term (or simply a rule language. RIF definesframe) if t, p1, ..., pn, v1, ..., vn, n 0, are simple, positional, or named-argument terms.
-
Externally defined terms. If t is a
concrete syntax onlyterm then External(t) is an externally defined term.
Such terms are used for exchanging rules,representing builtin functions and that syntax is XML-based, obtainedpredicates as a refinementwell as "procedurally attached" terms or predicates, which might exist in various rule-based systems, but are not specified by RIF. ☐
Membership, subclass, and serialization of the EBNF syntax. 2.6.1 EBNF for RIF-BLD Condition Language The Condition Language represents formulas that can beframe terms are used in the bodyto describe objects and class hierarchies.
3.3 Well-formedness of Terms
The RIF-BLD rules. Itset of all symbols, Const, is supposedpartitioned into
Each predicate and function symbol has precisely one arity.
-
The EBNF grammarFor positional symbols, an arity is a superset ofnon-negative integer that tells how many arguments the RIF-BLD condition language is as follows. CONDITION ::= 'And' '(' CONDITION* ')' | 'Or' '(' CONDITION* ')' | 'Exists' Var+ '(' CONDITION ')' | COMPOUND COMPOUND ::= Uniterm | Equal | Member | Subclass | Frame Uniterm ::= Const '(' (TERM* | (Const '->' TERM)*) ')' Equal ::= TERM '=' TERM Member ::= TERM '#' TERM Subclass ::= TERM '##' TERM Frame ::= TERM '[' (TERM '->' TERM)* ']' TERM ::= Const | Var | COMPOUND Const ::= LITERAL '^^' SYMSPACE Var ::= '?' VARNAME The production rulesymbol can take.
- For
the non-terminal CONDITION represents RIF condition formulas (defined earlier). The connectives And and Or define conjunctions and disjunctionssymbols that take named arguments, an arity is a set {s1 ... sk} of conditions, respectively. Exists introduces existentially quantified variables. Here Var+ standsargument names (si ArgNames), which are allowed for that symbol.
The listarity of variables that are freea symbol (or whether it is a predicate, a function, or an individual) is not specified in CONDITION .RIF-BLD conditions permit only existential variables, but RIF-FLD syntax allows arbitrary quantification, which can be usedexplicitly. Instead, it is inferred as follows. Each constant symbol in some dialects.a CONDITION can also beRIF-BLD formula (or a COMPOUND term, i.e.set of formulas) may occur in at most one context: as an individual, a Uniterm , Equal , Member , Subclass , or Frame . The production for the non-terminal TERM defines RIF-BLD terms -- constants, variables,function symbol of a particular arity, or COMPOUND terms. The RIF-BLD presentation syntax does not commit to anya predicate symbol of a particular vocabulary forarity. The namesarity of variables or forthe literals usedsymbol and its type is then determined by its context. If a symbol from Const occurs in constant symbols.more than one context in a set of formulas, the examples, variables are denoted by Unicode character sequences beginning with a ?-sign. Constant symbols haveset is not well-formed in RIF-BLD.
For a term of the form: LITERAL^^SYMSPACEform External(t) to be well-formed, t must be an instance of an external schema, where SYMSPACE isi.e., a schema of an IRI string that identifies the symbol spaceexternally specified term, as defined in Section Schemas for Externally Defined Terms of RIF-FLD.
Also, if a term of the constant and LITERALform External(p(...)) occurs as an atomic formula then the occurrence of p is considered to be a Unicode string frompredicate occurrence.
3.4 Formulas
Any term (positional or with named arguments.arguments) of the form p(...) (or External(p(...)), where p is a frame termpredicate symbol, is also an atomic formula. Equality, membership, subclass, and frame terms are also atomic formulas. A term composedformula of the form External(p(...)) is also called an object Idexternally defined atomic formula.
Simple terms (constants and variables) are not formulas. Not all atomic formulas are well-formed. A collection of attribute-value pairs. Example 1 shows conditionswell-formed atomic formula is an atomic formula that is also a well-formed term (see Section Well-formedness of Terms). More general formulas are composedconstructed out of uniterms, frames, and existentials.the examples ofatomic formulas with the frames showhelp of logical connectives.
Definition (Well-formed formula).
A well-formed formula is a statement that variables can occur in the syntactic positionshas one of object Ids, object properties, or property values. Example 1 (RIF-BLD conditions) We use the prefix bks to abbreviate http://example.com/books# and the prefix auth for http://example.com/authors#. Positional terms: book^^rif:local(auth:rifwg^^rif:iri bks:LeRif^^rif:iri) Exists ?X (book^^rif:local(?X LeRif^^rif:local)) Terms with named arguments: book^^rif:local(author^^rif:local->auth:rifwg^^rif:iri title^^rif:local->bks:LeRif^^rif:iri) Exists ?X (book^^rif:local(author^^rif:local->?X title^^rif:local->bks:LeRif^^rif:iri)) Frames: wd1^^rif:local[author^^rif:local->auth:rifwg^^rif:iri title^^rif:local->bks:LeRif^^rif:iri ] Exists ?X (wd2^^rif:local[author^^rif:local->?X title^^rif:local->bks:LeRif^^rif:iri ]) Exists ?X (wd2^^rif:local#book^^rif:local[author^^rif:local->?X title^^rif:local->bks:LeRif^^rif:iri]) Exists ?I ?X (?I[author^^rif:local->?X title^^rif:local->bks:LeRif^^rif:iri]) Exists ?I ?X (?I#book^^rif:local[author^^rif:local->?X title^^rif:local->bks:LeRif^^rif:iri]) Exists ?S (wd2^^rif:local[author^^rif:local->auth:rifwg^^rif:iri ?S->bks:LeRif^^rif:iri]) Exists ?X ?S (wd2^^rif:local[author^^rif:local->?X ?S->bks:LeRif^^rif:iri]) Exists ?I ?X ?S (?I#book^^rif:local[author->?X ?S->bks:LeRif^^rif:iri]) 2.6.2 EBNF for RIF-BLD Rule Language The presentation syntax for Horn rules extends the syntax in Section EBNF for RIF-BLD Condition Language withthe following productions. Ruleset ::= RULE* RULE ::= 'Forall' Var+ '(' RULE ')' | Implies | COMPOUND Implies ::= COMPOUND ':-' CONDITIONforms:
- Atomic: If is a
Rulesetwell-formed atomic formula then it is also a set of RIF rules. Rules are generated by the Implies production, with optional Forall -quantification. Varwell-formed formula.
- Conjunction: If 1,
COMPOUND..., n, and CONDITION were defined as part of the syntax for positive conditions in Section EBNF for RIF-BLD Condition Language . Note that COMPOUND terms are treated as rules with an empty condition part -- they are usually called facts . Note that, by a definition in Section Formulasn 0, atomic formulas that correspond to builtin predicates (i.e., formulas with signature bi_atomic )are not allowed in the conclusion part of a rule. This restrictionwell-formed formulas then so is not reflected in the EBNF syntax. The document RIF Use Cases and Requirements includesAnd(1 ... n), called a use case "Negotiating eBusiness Contracts Across Rule Platforms", which discussesconjunctive formula. As a business rule slightly modified here: If an itemspecial case, And() is perishableallowed and itis delivered to John more than 10 days after the scheduled delivery datetreated as a tautology, i.e., a formula that is always true.
- Disjunction: If 1, ..., n, n 0, are well-formed formulas then
the item will be rejected by him. In the Presentation EBNF Syntax used throughout this document, this rule can be written in one of these two equivalent ways: Example 2 (RIF-BLD rules) Hereso is Or(1 ... n), called a disjunctive formula. When n=0, we use the prefix pplget Or() as an abbreviation for http://example.com/people#. The prefix opa special case; it is used fortreated as a yet-to-be-determined IRI, which will be used for RIF builtin predicates. a. Universal form: Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays ( reject^^rif:local(ppl:John^^rif:iri ?item) :- And(perishable^^rif:local(?item) delivered^^rif:local(?item ?deliverydate ppl:John^^rif:iri) scheduled^^rif:local(?item ?scheduledate) fn:subtract-dateTimes-yielding-dayTimeDuration(?deliverydate ?scheduledate ?diffduration) fn:get-days-from-dayTimeDuration(?diffduration ?diffdays) op:numeric-greater-than(?diffdays 10)) ) b. Universal-existential form: Forall ?item ( reject^^rif:local(ppl#John^^rif:iri ?item ) :- Exists ?deliverydate ?scheduledate ?diffduration ?diffdays ( And(perishable^^rif:local(?item) delivered^^rif:local(?item ?deliverydate ppl:John^^rif:iri) scheduled^^rif:local(?item ?scheduledate) fn:subtract-dateTimes-yielding-dayTimeDuration(?deliverydate ?scheduledate ?diffduration) fn:get-days-from-dayTimeDuration(?diffduration ?diffdays) op:numeric-greater-than(?diffdays 10)) ) ) 2.7 XML Serialization for the Interchange of RIF-BLD The XML serialization for RIF-BLD presentation syntax given in this sectioncontradiction, i.e., a formula that is alternating or fully striped (e.g., Alternating Normal Form ). Positional informationalways false.
- Existentials: If is
optionally exploited only for the arg role elements. For example, role elements ( declare anda well-formed formula )and ?V1, ..., ?Vn are explicit withinvariables then Exists?V1 ...?Vn() is an existential formula.
Formulas constructed using the above definitions are called RIF-BLD conditions. The Exists element.following formulas lead to the examplesnotion of Java and RDF, we use capitalized names for class elementsa RIF-BLD rule.
-
Rule implication: If is an well-formed atomic formula and
namesis a RIF-BLD condition then :- is a well-formed formula, called rule implication, provided that start with lowercase for role elements. The all-uppercase classes inis not externally defined (i.e., does not have the presentation syntax, such as CONDITION , become XML entities. They act like macrosform External(...)).
-
Quantified rule: If is a rule implication and ?V1, ..., ?Vn are
not visiblevariables 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 instance markup.the other classes as wellprefix Forall?V1 ...?Vn. Quantified rules will also be referred to as non-terminalsRIF-BLD rules.
-
Group: If is a frame term and
symbols (such as Exists1, ..., n are RIF-BLD rules or =group formulas (they can be mixed) then Group (1 ... n) become XML elementsand 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 attributes, as shown below. 2.7.1 XML for RIF-BLD Condition Language We now serializeframe term . Note that some of the syntaxi's can be group formulas themselves, which means that groups can be nested. This allows one to attach metadata to various subsets of Section EBNF for RIF-BLD Condition Languagerules, which may be inside larger rule sets, which in XML. Classes, roles and their intended meaning - And (conjunction) - Or (disjunction) - Exists (quantified formulaturn can be annotated. ☐
It can be seen from the definitions that RIF-BLD has a wide variety of syntactic forms for 'Exists', containing declareterms and formula roles) - declare (declare role, containing a Var) - formula (formula role, containing a CONDITION formula) - Uniterm (term or atomic formula, positional or with named arguments) - Member (member formula) - Subclass (subclass formula) - Frame (Frame formula) - object (Member/Frame role containing a TERM or an object description) - op (Uniterm roleformulas. This provides the infrastructure for predicates/functions as operations) - arg (argument role) - upper (Member/Subclass upper class role) - lower (Member/Subclass lower instance/class role) - slot (Uniterm/Frame slot role, prefix version of slot infix ' -> ') - Equal (prefix versionexchanging rule languages that support rich collections of term equation '=') - side (Equal left-hand side and right-hand side role) - Const (slot, individual, function, or predicate symbol, with optional 'type' attribute) - Var (logic variable) For the XML Schema Definition (XSD)syntactic forms. Systems that do not support some of the RIF-BLD condition language see Appendix Specification . The XMLthat syntax for symbol spaces utilizes the type attribute associated with XML term elements such as Const .directly can still support it through syntactic transformations. For instance, a literaldisjunctions in the xsd:dateTime data typerule body can be representedeliminated through a standard transformation, such as <Const type="xsd:dateTime">2007-11-23T03:55:44-02:30</Const>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 following example illustrates XML serialization of RIF conditions. Example 3 (A RIF conditionarguments by their names and its XML serialization): We useincorporating them into the prefix bks as an abbreviationpredicate name. For http://example.com/books# and currinstance, p(bb->1 aa->2) can be represented as p_aa_bb(2,1).
3.5 EBNF Grammar for http://example.com/currencies# a. RIF condition And ( Exists ?Buyer ( purchase^^rif:local ( ?Buyer ?Seller book^^rif:local ( ?Author bks:LeRif^^rif:iri ) curr:USD^^rif:iri ( 49^^xsd:integer ) ) ?Seller=?Author ) b. XML serialization <And> <formula> <Exists> <declare><Var>Buyer</Var></declare> <formula> <Uniterm> <op><Const type="rif:local">purchase</Const></op> <arg><Var>Buyer</Var></arg> <arg><Var>Seller</Var></arg> <arg> <Uniterm> <op><Const type="rif:local">book</Const></op> <arg><Var>Author</Var></arg> <arg><Const type="rif:iri">bks:LeRif</Const></arg> </Uniterm> </arg> <arg> <Uniterm> <op><Const type="rif:iri">curr:USD</Const></op> <arg><Const type="xsd:integer">49</Const></arg> </Uniterm> </arg> </Uniterm> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And>the following example illustrates XML serializationPresentation Syntax of RIF conditions that involve terms with named arguments. Example 4 (A RIF condition and its XML serialization): We use the prefix bks to abbreviate http://example.com/books#, the prefix auth for http://example.com/authors#, and curr for http://example.com/currencies#, a. RIF condition: And ( Exists ?Buyer ?P ( ?P # purchase^^rif:local [ buyer^^rif:local -> ?Buyer seller^^rif:local -> ?Seller item^^rif:local -> book^^rif:local ( author^^rif:local -> ?Author title^^rif:local -> bks:LeRif^^rif:iri ) price^^rif:local -> 49^^xsd:integer currency^^rif:local -> curr:USD^^rif:iri ] ) ?Seller=?Author ) b. XML serialization: <And> <formula> <Exists> <declare><Var>Buyer</Var></declare> <declare><Var>P</Var></declare> <formula> <Frame> <object> <Member> <lower><Var>P</Var></lower> <upper><Const type="rif:local">purchase</Const></upper> </Member> </object> <slot><Const type="rif:local">buyer</Const><Var>Buyer</Var></slot> <slot><Const type="rif:local">seller</Const><Var>Seller</Var></slot> <slot> <Const type="rif:local">item</Const> <Uniterm> <op><Const type="rif:local">book</Const></op> <slot><Const type="rif:local">author</Const><Var>Author</Var></slot> <slot><Const type="rif:local">title</Const><Const type="rif:iri">bks:LeRif</Const></slot> </Uniterm> </slot> <slot><Const type="rif:local">price</Const><Const type="xsd:integer">49</Const></slot> <slot><Const type="rif:local">currency</Const><Const type="rif:iri">curr:USD</Const></slot> </Frame> </formula> </Exists> </formula> <formula> <Equal> <side><Var>Seller</Var></side> <side><Var>Author</Var></side> </Equal> </formula> </And> 2.7.2 XML for RIF-BLD Rule Language The following extends the XML syntax in Section XML for RIF-BLD Condition Language , by serializingRIF-BLD
So far, the syntax of Section EBNF forRIF-BLD Rule Languagehas been specified in XML. The Forall element contains the role elements declare and formula ,Mathematical English. Tool developers, however, may prefer EBNF notation, which were earlier used withinprovides a more succinct overview of the Exists elementsyntax. Several points should be kept in Section XML for RIF-BLD Condition Language . The Implies element containsmind regarding this notation.
- The
role elements if and then to designate these two partssyntax of a rule. Classes, roles and their intended meaning - Ruleset (rule collection, containing rule roles) - Forall (quantified formula for 'Forall', containing declare and formula roles) - Implies (implication, containing if and then roles) - if (antecedent role, containing CONDITION) - then (consequent role, containing a Uniterm, Equal, or Frame) Forfirst-order logic is not context-free, so EBNF does not capture the XML Schema Definition (XSD)syntax of theRIF-BLD Horn rule language see Appendix Specification .precisely. For instance, it cannot capture the rulesection on well-formedness conditions, i.e., the requirement that each symbol in Example 5aRIF-BLD can be serializedoccur in XML as shown belowat most one context. As a result, the first element ofEBNF grammar defines a rule set whose second elementstrict 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
business rule for Fred. Example 5 (A RIF rule set in XML syntax) <Ruleset> <rule> <Forall> <declare><Var>item</Var></declare> <declare><Var>deliverydate</Var></declare> <declare><Var>scheduledate</Var></declare> <declare><Var>diffduration</Var></declare> <declare><Var>diffdays</Var></declare> <formula> <Implies> <if> <And> <formula> <Uniterm> <op><Const type="rif:local">perishable</Const></op> <arg><Var>item</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">delivered</Const></op> <arg><Var>item</Var></arg> <arg><Var>deliverydate</Var></arg> <arg><Const type="rif:iri">ppl:John</Const></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">scheduled</Const></op> <arg><Var>item</Var></arg> <arg><Var>scheduledate</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">fn:subtract-dateTimes-yielding-dayTimeDuration</Const></op> <arg><Var>deliverydate</Var></arg> <arg><Var>scheduledate</Var></arg> <arg><Var>diffduration</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">fn:get-days-from-dayTimeDuration</Const></op> <arg><Var>diffduration</Var></arg> <arg><Var>diffdays</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:iri">op:numeric-greater-than</Const></op> <arg><Var>diffdays</Var></arg> <arg><Const type="xsd:long">10</Const></arg> </Uniterm> </formula> </And> </if> <then> <Uniterm> <op><Const type="xsd:long">reject</Const></op> <arg><Const type="rif:iri">ppl:John</Const></arg> <arg><Var>item</Var></arg> </Uniterm> </then> </Implies> </formula> </Forall> </rule> <rule> <Forall> <declare><Var>item</Var></declare> <formula> <Implies> <if> <Uniterm> <op><Const type="rif:local">unsolicited</Const></op> <arg><Var>item</Var></arg> </Uniterm> </if> <then> <Uniterm> <op><Const type="rif:local">reject</Const></op> <arg><Const type="rif:iri">ppl:Fred</Const></arg> <arg><Var>item</Var></arg> </Uniterm> </then> </Implies> </formula> </Forall> </rule> </Ruleset> 2.8 Translation Betweenconcrete syntax: it does not address the RIF-BLD Presentation and XML Syntaxes We now showdetails of how to translate betweenconstants 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 TERMTERM...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 XML syntaxesfor illustration of RIF-BLD. 2.8.1 Translationthe 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 translation betweenCondition Language represents formulas that can be used in the presentation syntax andbody of the XML syntaxRIF-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 given by a tableas follows.
Presentation Syntax XML Syntax And ( conjunct 1 . . . conjunct n ) <And> <formula> conjunct 1 </formula> . . . <formula> conjunct n </formula> </And> Or ( disjunct 1 . . . disjunct n ) <Or> <formula> disjunct 1 </formula> . . . <formula> disjunct n </formula> </Or> Exists variable 1 . . . variable n ( body ) <Exists> <declare>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, cConst, denotes an individual then it is required that
IC(c)Dind.
- If cConst, 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->ba->b]. Such repetitions arise naturally when variables are instantiated with constants. For instance, o[?A->?B?A->?B] becomes o[a->ba->b] if variable 1 </declare>?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.
<declare>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
n </declare> <formula> body </formula> </Exists> predfuncin Var
-
I(
argumentf(t1 . . . argument... tn) <Uniterm> <op> predfunc </op> <arg> argument) = IF(I(f))(I(t1 </arg> . . . <arg> argument),...,I(tn </arg> </Uniterm> predfunc))
-
I(
keyf(s1 -> filler->v1 . . . key... sn -> filler->vn) <Uniterm> <op> predfunc </op> <slot> key 1 filler 1 </slot> . . . <slot> key n filler n </slot> </Uniterm> inst [ key 1 -> filler 1 . . . key n -> filler n ] <Frame> <object> inst </object> <slot> key 1 filler 1 </slot> . . . <slot> key n filler n </slot> </Frame> inst # class [ key 1 -> filler 1 . . . key n -> filler n ] <Frame> <object> <Member> <lower> inst </lower> <upper> class </upper> </Member> </object> <slot> key) = ISF(I(f))({<s1 filler,I(v1 </slot> . . . <slot> key)>,...,<sn filler,I(vn </slot> </Frame> sub ## super [ key)>})
Here we use {...} to denote a set of argument/value pairs.
-
I(o[a1
-> filler->v1 . . . key n -> filler n... ak->vk] <Frame> <object> <Subclass> <lower> sub </lower> <upper> super </upper> </Subclass> </object> <slot> key) = Iframe(I(o))({<I(a1 filler),I(v1 </slot> . . . <slot> key)>, ..., <I(an filler),I(vn </slot> </Frame> inst # class <Member> <lower> inst </lower> <upper> class </upper> </Member> sub ## super <Subclass> <lower>)>})
Here {...} denotes a bag of attribute/value pairs.
-
I(c1##c2) = Isub
</lower> <upper> super </upper> </Subclass> left(I(c1), I(c2))
-
I(o#c) =
right <Equal> <side> left </side> <side> right </side> </Equal> name ^^ space <Const type=" space "> name </Const> ? name <Var> name </Var> 2.8.2 Translation of RIF-BLD Rule Language The translation between the presentation syntax and the XML syntax of the RIF-BLD Rule LanguageIisa(I(o), I(c))
-
I(x=y) = I=(I(x), I(y))
-
I(External(t)) = Iexternsl()(I(s1), ..., I(sn)), if t is
given by a table that extends the translation table of Section Translationan instance of RIF-BLD Condition Language as follows. Presentation Syntax XML Syntax Ruleset ( clausethe external schema = (?X1 . . . clause...?Xn ) <Ruleset> <rule> clause;) by substitution ?X1 </rule> . . . <rule> clause/s1 ...?Xn </rule> </Ruleset> Forall variable/s1.
. . variable nNote 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( ruleExternal(t)) <Forall> <declare> variable 1 </declare> . . . <declare> variable n </declare> <formula> rule </formula> </Forall> conclusion :- condition <Implies> <if> condition </if> <then> conclusion </then> </Implies> 2.9 Subdialectsis well-defined.
The effect of data types. The data types in DTS impose the following restrictions. If dt is a symbol space identifier of RIF-BLD This isa proposal to specify RIF-CORE etc. by just removing syntactic constructs from RIF-BLD (hence, throughdata type, let LSdt denote the effectlexical space of the syntaxdt, restrictingVSdt denote its value space, and Ldt: LSdt VSdt the semantics).lexical-to-value-space mapping (for the point is that it makes more sense for most engines to support only some subdialectsdefinitions of these concepts, see Section Primitive Data Types of BLD,RIF-FLD). Then the following must hold:
- VSdt Dind; and
- For each constant "lit"^^dt LSdt, IC("lit"^^dt) = Ldt(lit).
That subdialects and fragments of BLD are reused inis, IC must map the definitionconstants of other RIF dialects. ***a data type dt in accordance with Ldt.
RIF-BLD does not impose restrictions on IC for constants in the syntactic structurelexical spaces that do not correspond to primitive datatypes in DTS. ☐
4.3 Interpretation of RIF-BLD suggests several useful subdialects: RIF-COREFormulas
Definition (Truth valuation).
This subdialect is obtained fromTruth valuation for well-formed formulas in RIF-BLD by removing support for: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)).
- To ensure that equality
formulas inhas precisely the rule conclusions (while still allowing them in conditions) terms with named arguments ??? membership, subclass,expected properties, it is required that:
Itruth(I(x=y)) = t if and frame terms ??? RIF-CORE+equality . This subdialect extends RIF-CORE by adding support for equality formulas in the rule conclusions. RIF-CORE+named arguments . This subdialect extends RIF-CORE by adding syntactic support for terms with named arguments.only if frames are not included in RIF-CORE / RIF-CORECOND then extensions of RIF-CORE / RIF-CORECOND with frames are added here. 3 RIF-BLD Semantics 3.1 The Semantics of RIF-BLD as a Specialization of RIF-FLD This section defines the precise relationship between the semantics of RIF-BLDI(x) = I(y) and the semantic framework of RIF-FLD. The remaining sections describe the semantics of RIF-BLD without referringthat Itruth(I(x=y)) = f otherwise.
- This is tantamount to saying that TValI(x=y) = t if I(x) = I(y).
- Subclass: TValI(sc##cl) = Itruth(I(sc##cl)).
To ensure that the general framework -- except for Primitive Data Types whose definitionoperator ## is not duplicated here. The semantics oftransitive, i.e., c1##c2 and c2##c3 imply c1##c3, the RIF Basic Logic Dialectfollowing is defined by specialization from the semantics of the [:FLD/Semantics:Semantic Frameworkrequired:
For Logic Dialects] of RIF. Section [:FLD/Semantics#sec-rif-dialect-semantics:Semantics of a RIF Dialect as a Specialization of RIF-FLD] in that document lists the parameters of the semantic framework, which we needall 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 specialize for RIF-BLD. Recallensure that the semanticsall members of a dialect is derived from these notions by specializing the following parameters. The effectsubclass are also members of the syntax . RIF-BLD does not support negation. Thissuperclass, 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 only obvious simplification with respectdifferent attribute/value pairs are supposed to RIF-FLD as farbe understood as conjunctions, the semanticsfollowing is concerned. Truth values . The set TV of truth values in RIF-BLD consists of just two values,required:
TValI(o[a1->v1 ... ak->vk]) = t if and f such that f < t t . Clearly, <only if TValI(o[a1->v1]) = ... = TValI(o[ak->vk]) = 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-FLDExternally defined atomic formula: TValI(External(t)) = Itruth(Iexternal()(I(s1), ..., I(sn))), if t is defined with respect toan unspecified set of intended semantic structures andatomic formula that dialects of RIF must make this notion concrete. For RIF-BLD, this setis defined in one of the two following equivalent ways: as a setan instance of all models; or asthe unique minimal model. These two definitions are equivalent for entailment of RIF-BLD conditionsexternal schema = (?X1 ...?Xn; ) by RIF-BLD rulesets, since all rules in RIF-BLD are Horn -- itsubstitution ?X1/s1 ...?Xn/s1.
Note that, by definition, External(t) is a classical resultwell-formed only if t is an instance of Van Emden and Kowalski [ vEK76 ]. 3.2 Truth Valuesan external schema. Furthermore, by the set TVdefinition of truth values in RIF-BLD consistscoherent sets of just two values,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
and f.
This set hasThe empty disjunction is treated as a total order, called truth order , such thatcontradiction, so TValI(Or()) = f <.
- Quantification:
- TValI(Exists?v1 ...?vn ()) = t if and only if for some I*, described below, TValI*() = t.
-
3.3 Semantic Structures A semantic structure ,TValI ,(Forall?v1 ...?vn ()) = t if and only if for every I*, described below, TValI*() = t.
Here I* is a tuplesemantic structure of the form <TV, DTS, D, Dind, Dfunc, IC, I*V, IF, Iframe, ISF, Isub, Iisa, I=, Iexternsl, Itruth >. Here D>, which is a non-empty set of elements called the domain ofexactly like I, and there is a proper subset, D ind ⊂ Dexcept that the mapping I*V, whichis used to interpret individuals. We use Const to refer to the setinstead of all constant symbols and Var to referIV. I*V is defined to the set ofcoincide with IV on 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 invariables except, possibly, on ?v1,...,?vn.
- Rule implication:
-
TValI
(please refer to Section Primitive Data Types of RIF-FLD for the semantics of data types). The other components of(conclusion:- condition) = t, if either TValI are total mappings defined as follows:(conclusion)=t or TValI C maps Const to elements(condition)=f.
-
TValI(conclusion:- condition) = f otherwise.
- Groups of
D . This mapping interprets constant symbols.rules:
If is a constant, c ∈ Const , occurs in the positiongroup formula of an individualthe form Group (1 ... n) or Group (1 ... n) then
-
it is required thatTValI C( c ) ∈ D ind .) = t if and only if TValI V maps Var to elements of D ind(1) = t, ..., TValI(n) = t.
-
This mapping interprets variable symbols.TValI() = f maps D to functions D* → D (here D* isotherwise.
This means that a setgroup of all sequencesrules is treated as a conjunction. The metadata is ignored for purposes of any finite length overthe domain DRIF-BLD semantics.
A model of a group of rules, , is a semantic structure I such that TValI() = t. In this mapping interprets positional terms.case, we write I SF interprets terms|=. ☐
Note that although metadata associated with named arguments.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 total mapping from Const to theset of total functionsRIF-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 form SetOfFiniteBagscase that TValI( ArgNames × D) → D= t.
This is analogous toEquivalently, we can say that |= holds iff whenever I|= it follows that also I|=. ☐
5 XML Serialization Syntax for RIF-BLD
The interpretation of positional terms with two differences: Each pair <s,v> ∈ ArgNames × D represents a argument/value pair instead of just a valueXML serialization for RIF-BLD given in the case of athis section is alternating or fully striped (e.g., [ANF01]). Positional term.information is optionally exploited only for the arguments of a term with named arguments constitute a finite bag of argument/value pairs rather than a finite ordered sequence of simplearg role elements. Bags (multisets)For example, role elements (declare and formula) are used here becauseexplicit within the order ofExists element. Following the argument/value pairs in a term with named arguments is immaterialexamples of Java and the pairs may repeat.RDF, we use capitalized names for instance, p(a->b a->b) . I frame is a total mapping from D to total functions ofclass elements and names that start with lowercase for role elements.
The form SetOfFiniteBags ( D × D ) → D . This mapping interprets frame terms. An argument, d ∈ Dall-uppercase classes in the presentation syntax, such as FORMULA, to I frame represent an objectbecome XML entities. They act like macros and are not visible in instance markup. The finite bag {<a1,v1>, ..., <ak,vk>} represents a bag of attribute-value pairsother classes as well as non-terminals and symbols (such as Exists or =) become XML elements with optional attributes, as shown below.
5.1 XML for d .RIF-BLD Condition Language
We will see shortly how I frame is used to determine the truth valuation of frame terms. Bags are used here becausenow serialize the ordersyntax of the attribute/value pairsSection EBNF for RIF-BLD Condition Language in a frame is immaterialXML.
Classes, roles and pairs may repeat. For instance, o[a->b a->b] . I sub givestheir intended meaning
to the subclass relationship. It is a total function D × D → D . The operator ## is required to be transitive, i.e., c1 ## c2- And c2 ## c3 must imply c1 ## c3 . This is ensured by(conjunction)
- Or (disjunction)
- Exists (quantified formula for 'Exists', containing declare and formula roles)
- declare (declare role, containing a restriction in Section Interpretation of Formulas . I isa gives meaning toVar)
- 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 membership. It isrole)
- lower (Member/Subclass lower instance/class role)
- slot (Atom/Expr/Frame slot role, containing a total function D × D → D . The relationships # and ## are required to have the usual property that all membersProp)
- Prop (Property, prefix version of slot infix '->')
- key (Prop key role, containing a subclass are also membersConst)
- 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 superclass, i.e., o # cl and cl ## scl must imply o # scl . This is ensured by a restriction in Section InterpretationXML Schema Definition (XSD) of Formulas . I = gives meaning tothe equality. It is a total function D × D → D . I Truth is a total mapping D → TVRIF-BLD condition language see Appendix XML Schema for BLD.
It is used to define truth valuation of formulas. We also defineThe following mapping I : I (k) = I C (k), if k is aXML syntax for symbol inspaces utilizes the type attribute associated with XML term elements such as Const I (?v) = I V (?v), if ?v is. For instance, a variableliteral in Var I (f(t 1 ... t n )) = I F ( I (f))( I (t 1 ),..., I (t n )) I (f( s 1 ->v 1 ... s n ->v n )) = I SF ( I (f))({ <s 1 , I (v 1 ) > ,..., <s n , I (v n ) > }) Here we use {...} to denote a bag of argument/value pairs. I ( o[a 1 ->v 1 ... a k ->v k ] ) = I frame ( I ( o ))({ < I ( a 1 ), I (v 1 ) > , ..., < I ( a n ), I (v nthe xsd:dateTime data type can be represented as <Consttype="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 )
> }) Here {...} denotes a bagXML 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 attribute/value pairs. I ( c1##c2 ) = I sub ( I ( c1 ), I ( c2 )) I ( o#c ) = I isa ( I ( o ), I ( c )) I ( x=y ) = I =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 (
I (x), I (y))?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
The effect of data types.following extends the data typesXML syntax in DTS imposeSection XML for RIF-BLD Condition Language, by serializing the following restrictions. If dt is a symbol space identifiersyntax of a data type, let LS dt denoteSection EBNF for RIF-BLD Rule Language in XML. The lexical space of dt , VS dt denote its value space,Forall element contains the role elements declare and L dt : LS dt → VS dtformula, which were earlier used within the lexical-to-value-space mapping (forExists element in Section XML for RIF-BLD Condition Language. The definitions ofImplies element contains the role elements if and then to designate these concepts, see Section Primitive Data Typestwo parts of RIF-FLD). Then the following must hold: VS dt ⊆ D ;a rule.
Classes, roles and their intended meaning
- 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 For each constant lit^^dt ∈ LS dt , I C ( lit^^dt ) = L dt ( lit ). That is, I C must mapformula roles)
- Implies (implication, containing if and then roles)
- if (antecedent role, containing FORMULA)
- then (consequent role, containing ATOMIC)
The constantsXML Schema Definition of a data type dtRIF-BLD is given in accordance with L dtAppendix XML Schema for BLD.
Example 6 (Serializing a RIF-BLD does not impose restrictions on I Cgroup annotated with metadata).
This example shows a serialization for constants inthe lexical spaces that do not correspond to primitive datatypes in DTS . 3.4 Interpretation of Formulas Truth valuationgroup from Example 3. For well-formed formulas in RIF-BLD is determined using the following function, denoted TVal I : Positional atomic formulas : TVal I ( r(t 1 ... t n )) = I Truth ( I ( r(t 1 ... t n ))) Atomic formulas with named arguments : TVal I ( p(s 1 ->v 1 ... s k ->v k )) = I Truth ( I ( p(s 1 -> v 1 ... s k ->v k ))). Equality : TVal I ( x = y ) = I Truth ( I ( x = y )). To ensure that equality has preciselyconvenience, the expected properties, itgroup is required that I Truth ( I ( x = y )) = t if and only if I ( x ) = I ( y )reproduced at the top and that I Truth ( I ( x = y )) = f otherwise. Subclass : TVal I ( sc ## cl ) = I Truth ( Ithen 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 (
sc ## cl ))."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 ensure thattranslate between the operator ## is transitive, i.e., c1 ## c2presentation and c2 ## c3 imply c1 ## c3 ,XML syntaxes of RIF-BLD.
5.3.1 Translation of RIF-BLD Condition Language
The followingtranslation between the presentation syntax and the XML syntax of the RIF-BLD Condition Language is required: For all c1 , c2 , c3 ∈ D , min t ( TVal I ( c1 ## c2 ), TVal I ( c2 ## c3 )) ≤ t TVal I ( c1 ## c3 ). Membership : TVal I ( o # cl ) = I Truth ( I ( o # cl )).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 ensurethis end, in the translation table, the positional and named argument terms that all membersoccur in the context of a subclassatomic formulas are also membersdenoted by the expressions of the superclass, i.e., o # clform pred(...) and cl ## scl implies o # scl ,the following is required: For all o , cl , scl ∈ D , min t ( TVal I ( o # cl ), TVal Iterms 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 (
cl ## scl )) ≤ t TVal Iconjunct1
. . .
conjunctn
)
|
<And>
<formula>conjunct1'</formula>
. . .
<formula>conjunctn'</formula>
</And>
|
Or (
o # scl ). Frame : TVal Idisjunct1
. . .
disjunctn
)
|
<Or>
<formula>disjunct1'</formula>
. . .
<formula>disjunctn'</formula>
</Or>
|
Exists
variable1
. . .
variablen (
o[abody
)
|
<Exists>
<declare>variable1 ->v'</declare>
. . .
<declare>variablen'</declare>
<formula>body'</formula>
</Exists>
|
pred (
argument1
... a k ->v k ]. . .
argumentn
)
|
= I Truth<Atom>
<op>pred'</op>
<arg>argument1'</arg>
. . .
<arg> argumentn'</arg>
</Atom>
|
External (
Iatomexpr
)
|
<External>
<content>atomexpr'</content>
</External>
|
func (
o[aargument1
->v. . .
argumentn
)
|
<Expr>
<op>func'</op>
<arg>argument1 ... a k ->v k ] )). Since the different attribute/value pairs are supposed to be understood as conjunctions, the following is required: TVal I'</arg>
. . .
<arg> argumentn'</arg>
</Expr>
|
pred (
o[aunicode1 ->v-> filler1
... a k ->v k ]. . .
unicoden -> fillern
)
|
= min t ( TVal I ( o[a<Atom>
<op>pred'</op>
<slot>
<Prop>
<key><Name>unicode1 ->v</Name></key>
<val>filler1 ] ), ..., TVal I ( o[a k ->v k ] )) Conjunction : TVal I'</val>
</Prop>
</slot>
. . .
<slot>
<Prop>
<key><Name>unicoden</Name></key>
<val>fillern'</val>
</Prop>
</slot>
</Atom>
|
func (
And( cunicode1 ... c-> filler1
. . .
unicoden -> fillern
)
|
) = min t ( TVal I (c<Expr>
<op>func'</op>
<slot>
<Prop>
<key><Name>unicode1 ), ..., TVal I (c</Name></key>
<val>filler1'</val>
</Prop>
</slot>
. . .
<slot>
<Prop>
<key><Name>unicoden )). Disjunction : TVal I ( Or( c</Name></key>
<val>fillern'</val>
</Prop>
</slot>
</Expr>
|
inst [
key1 ... c-> filler1
. . .
keyn ) ) = max t ( TVal I (c-> fillern
]
|
<Frame>
<object>inst'</object>
<slot>
<Prop>
<key>key1 ), ..., TVal I (c'</key>
<val>filler1'</val>
</Prop>
</slot>
. . .
<slot>
<Prop>
<key>keyn )). Quantification : TVal I ( Exists ?v'</key>
<val>fillern'</val>
</Prop>
</slot>
</Frame>
|
inst # class [
key1 ... ?v-> filler1
. . .
keyn (φ)) = max t ( TVal I* (φ)) and TVal I ( Forall ?v-> fillern
]
|
<Frame>
<object>
<Member>
<lower>inst'</lower>
<upper>class'</upper>
</Member>
</object>
<slot>
<Prop>
<key>key1 ... ?v'</key>
<val>filler1'</val>
</Prop>
</slot>
. . .
<slot>
<Prop>
<key>keyn (φ)) = min t ( TVal I* (φ)). Here max t (respectively, min t ) is taken over all interpretations I * of the form < TV , DTS , D , I C , I * V , I F , I frame , I SF , I'</key>
<val>fillern'</val>
</Prop>
</slot>
</Frame>
|
sub , I isa , I Truth >, which are exactly like I , except that the mapping I * V , is used instead of I V . I * V is defined to coincide with I V on all variables except, possibly, on ?v## super [
key1 ,..., ?v-> filler1
. . .
keyn -> fillern
]
|
<Frame>
<object>
<Subclass>
<lower>sub'</lower>
<upper>super'</upper>
</Subclass>
</object>
<slot>
<Prop>
<key>key1'</key>
<val>filler1'</val>
</Prop>
</slot>
. Rules : TVal I ( conclusion :- condition ) = t , if TVal I ( conclusion ) ≥ t TVal I ( condition ); TVal I ( conclusion :- condition ) = f otherwise. A model of a set Ψ of formulas is a semantic structure I such that TVal I (φ). .
<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 = t for every φ∈Ψ. In this case, we write I |= Ψ. 3.5 Logical Entailment We now define what it means for a set of RIF-BLD rules to entail a RIF-BLD condition. Let R be a setright
|
<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 rules and φ an existentially closed RIF-BLD condition formula. We say that R entails φ, written as R |= φ, if and only if for every semantic structure I of RRule Language
The translation between the presentation syntax and every ψ ∈ R , itthe XML syntax of the RIF-BLD Rule Language is given by the case that TVal I (ψ) ≤ TVal I (φ). Equivalently, we can say that R |= φ holds iff whenever I |= R it follows that also I |= φ. 4table 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>
|