RIF Basic Logic Dialect

The languagesublanguage of positive RIFconditions in RIF-BLD determines what can appear as a body (the if-part)of a rule (also known as the if-part, antecedent, or condition part of the rule) supported by the basic RIF logic.RIF-BLD. As explained in Section Overview, RIF's Basic Logic DialectRIF-BLD corresponds to definite Horn rules, and the bodies of such rules are conjunctions of atomic formulas without negation. However, it is well-known that disjunctions of such conditions can also be used in the bodies of rules without changing the essential properties of the rule language. This is based on the fundamental logical tautologies (h ← b ∨ c) ≡ ((h ← b) ∧ (h ← c)) and ∀ x (F ∧ G) ≡ (∀ x F ∧ ∀ x G). In other words, a rule with a disjunction in the body can be split into two or more rules that have no such disjunction.

The condition language is intended to be shared among the bodies of the rules expressed in future RIF dialects, such as LP, FO, PR and RR. The condition language might also be used to uniformly express integrity contraints and queries. This section presents a syntax and semantics for the RIF condition language.To make RIF dialects suitable as Web languages, RIF supports XML Schema primitive data types and some other primitivedata types. In addition, RIF promotes the use of Internationalized Resource Identifiers (or IRIs) RFC 3987 to refer to individuals, predicates, and functions.

To ensure extensibility and to provide for future higher-order dialects based on formalisms,formalisms such as HiLog and Common Logic, the RIF logic language does not draw a sharp boundary between the symbols used to denote individuals from symbols used as names for functions or predicates. Instead, all constant, preficate,predicate, and function symbols are drawn from the same universal set. RIF dialects control the contexts in which the different symbols can occur by attaching signatures to these symbols.

RIF's basic logic dialectRIF-BLD carefully selects signatures for the symbols so that the corresponding logic will be first-order: each symbol has a unique role as a symbol that represents an individual,individual object, a function symbol of a particular arity, or a predicate symbol of a particular arity. However, dialects extending the basic logicRIF-BLD will be allowed to use signatures in less restrictive fashions so that symbols could be polymorphic, polyadic, andpolymorphic (i.e. be allowed to occur in several different contexts (for example, bothcontexts; e.g., as individuals and as predicates).predicates) and polyadic (i.e take a varying number of arguments).

We begin by describing a syntax, which is more general than what the basic logic dialectRIF-BLD permits. This syntax can be used in the various dialects that extend RIF's basic logic dialect.RIF-BLD. Then we introduce the notion of a signature and specify the restrictions on the way signatures are allowed to be assigned to symbols. Next we define the presentation syntax using EBNF and describe the corresponding XML-based exchange syntax. Finally, we give a model-theoretic semantics to RIF-BLD.

2.1.1. Syntax

In this document we will introduce severaltwo related but distinct syntaxes:

• FormalPresentation syntax. This syntax is used in formal definitions, especially for the definitions and follows the standard textbook conventions for logical syntax. Presentation syntax. This syntax is closely related to the formal syntax and is derived fromsemantics. It by elaborating on the various aspects of RIF (such as, for example, data types). Thisis a human-oriented syntax, whichsyntax and, therefore, we use it in our the examples. Abstract syntax. This is a normative version ofthe RIF syntax. It is also derived frommodel theory and the formal syntax, but is more verbose thanexamples. The presentation syntax (this verbose nature of the abstract syntaxis the main reasonnot meant to be used for the presentation syntax).exchange of RIF rules.

• XML syntax. This syntax is the normative XML serialization of the abstractpresentation syntax. The key features of this syntax are derived from the presentation syntax, but some aspects related to rule exchange do not have counterparts in the presentation syntax.

2.1.1.1. Formal PreliminariesSymbols and Signatures

The languagealphabet of RIF Condition Language consists of a countably infinite set of constant symbols Const, a countably infinite set of variable symbols Var (disjoint from Const), connective symbols ∧And ∨, quantifier ∃,and Or, quantifier Exists, auxiliary symbols like (, ),symbols, such as "(" and so on.")". In the RIF presentation syntax, variables are written as Unicode strings preceded with the symbol "?". The syntax for constant symbols is given in Section Symbol Spaces below.

The language of RIF-BLD is the set of formulas constructed using the above alphabet according to the rules spelled out below.

The basic language construct is called term, which is defined inductively as follows:

• If t ∈ Const or t ∈ Var then t is a term.

• If t and t₁, ..., t_n are terms then t ( tt ( t₁ ... t_n ) is a termterm.

This definition is very general. It makes no distinction between constant symbols that represent individuals, predicates, and function symbols. The same symbol can occur in multiple contexts at the same time. For instance, p(p(a) p(a b c))if p, a, and b are symbols then p ( p ( a ) p ( a p c ) ) is a term. Even variables and general terms are allowed to occur in the position of predicates and function symbols. For instance, p(a)(p(b c) q)symbols, so p ( a ) ( ?v ( a c ) p ) is also a term. To control the context in which any given symbol can occur in a RIF dialects,dialect, the language associates a signature with each symbol (both constant and variable symbols).

Signatures. Let SigNames be a non-emptynon-empty, partially-ordered finite or countably infinite set of signature names. We require that this set includes at least the following signature names: i and bool . The signature name i represents the context where the constants that denote individual objects are allowed to appear. Thename boolatomic, which represents the context of atomic formulas. ADialects are free to introduce additional signature names. For instance, as we shall soon see, RIF-BLD also introduces another signature, term{ }. The partial order on SigNames is a statement ofdialect-specific (see, the form η{ especifics for RIF-BLD later); it is used in the definition of well-formed terms below.

We use the symbol < to represent the partial order on SigNames. Informally, α < β means that terms with signature α can be used wherever terms with signature β are allowed.

A signature is a statement of the form η{e₁ ..., ..., e_n, ...} where η ∈ SigNames is the name of the signature and {e₁ ..., ..., e_n, ...} is a countable set of signaturearrow expressions. ThisSuch a set can thus be empty,infinite, finite, or countably infinite.even empty. In RIF's basic logic dialect, this set willRIF-BLD, signatures can have at most one expression, but in more expressivearrow expression. Other dialects a signature can have(such as HiLog, for example) may require polymorphic symbols and thus allow signatures with more than one expression, and in this way they can support polymorphism. A signature expression can be a base signature expression or anarrow signatureexpression (as a special case,in them.

An arrow expression can be a Boolean signature expression ),is defined as follows, wherefollows:

• If κ, κ₁, ..., κ_n, and κn≥0, are signature names from SigNames : i and bool are basic signature expressions ., then (κ₁ ... κ_n) ⇒ κ, where n≥0,κ is an arrow signatureexpression. In particular, () ⇒ iterm and ( iterm) ⇒ iterm are arrow signatureexpressions.

• If κ above is boolatomic then the signature is called a Boolean signatureexpression.

A set S of signatures is said to becoherent if itiff

• S contains the signatures i { } and bool { },special signature atomic{ }, which representrepresents the context of individual objects andatomic formulas; and

• no two different signatures inS have the samehas at most one signature for any given signature name.

• Well-formed termsWhenever S contains a pair of signatures, ηS and formulas. RIF uses signatures to controlκR, such that η<κ then R⊆S. Here ηS denotes a signature with the context in which terms can appear throughname η and the notionassociated set of well-formed terms and well-formed atomic formulas. First, as mentioned above, eacharrow expression S; similarly κR is a signature named κ with the set of expressions R. The requirement that R⊆S ensures that symbols that have signature η can be used wherever the symbols with signature κ are allowed.

2.1.1.2. Well-formed Terms and Formulas

Signatures help control the context in which various symbols can occur through the notion of well-formed formulas. First, as mentioned above, each constant and variable symbol (constant or variable)is associated with exactly one signature from a coherent set of signatures. (DifferentDifferent symbols can be associated with the same signature, but oneno symbol cannotcan be associated with more than one signature.) If σ is asignature. Since signature thennames uniquely identify signatures in coherent signature sets, we will often use σ #signature names to denote the name ofrefer to signatures. For instance, we may say that signature.symbol f has signature atomic rather than that "f has signature atomic{ }" or that "f has signature named atomic."

• If s is a constant or variable symbol with signature η{...} and a base expression i or bool belongs to the set {...} associated with that signatureη then s is a well-formed term with signature i { } or bool { }, respectively. Noteη.

• A term t ( t₁ ... t_n ), 0≤n, is a well-formed term whose signature is σ iff

  • t is a well-formed term that if symbol shas a signature, say, κ{ i ( i )⇒ bool }which contains an arrow expression of the form (σ₁ ... σ_n) ⇒ σ; and

  • symbolEach t _hasi is a well-formed term whose signature ρ{(is σ'_i )⇒, such that σ'_i (, < σ_i )⇒ bool } then, according to the above definition, s.

  • As a special case, when n=0 we obtain that t ( ) is a well-formed term, while t is not. Also, according to this definition theterm with signature of a symbol can be different from theσ, if t's signature ofcontains the same symbol when it is viewed as a term. For instance, in the above example, s has a signature κ{ i ( i )⇒ bool } as a symbol, but its signature as a term is i { }. Furthermore, a symbol always has just one signature (which might have many arrow expressions in it), but a term can have several signatures. For instance, if symbol q has the signature δ{ i bool } then q as a well-formed term has two signatures: i { } and bool { }. Although some symbols can have signatures as symbols and signatures as terms, it will be clear from the context which signature is meant. Complex terms (defined below) are not symbols and so they can have signatures only as terms. A term t ( t 1 ... t n ) is a well-formed term with signature σ iff t is a well-formed term with signature σ 0 ; Each t i is a well-formed term with signature σ j , j = 1,...,n (the σ j 's are not necessarily distinct); and σ 0 contains anarrow expression of the form (σ 1 # ... σ n # )() ⇒ σ #σ.

• A term t ( tt ( t₁ ... t_n ) is a well-formed atomic formula iff it is a well-formed term with the signature bool { }.atomic.

Note that f()according to the above definition f ( ) and f are distinct terms andterms.

More general formulas are constructed out of atomic formulas with the proposed XML serialization also treats these as distinct fragmentshelp of XML:logical connectives. The nullary function application <Uniterm><Const>f</Const></Uniterm> vs.condition sublanguage of RIF-BLD defines the symbol <Const>f</Const>following general well-formed condition formulas.

• RIF defines that thereIf φ is a special predicate, = , which denotes equality. Like other predicateswell-formed atomic formula then it hasis also a signature, and this signature includes the Boolean expression ( i iwell-formed condition formula.

• If are φ₁, ..., φ_n, n ≥ 0, are well-formed condition formulas then so is And ( φ₁ ... φ_n ) ⇒ bool. As a special case, And ( ) is allowed and possibly other expressions of the form ( s s ) ⇒ bool , where sis treated as a signature name. No other signaturestautology true.

• If φ₁, ..., φ_n, n ≥ 0, are allowed for =well-formed condition formulas then so is Or ( φ₁ ... φ_n ). When n=0, we note thatget Or ( ) as a special case; it is common practice to write the atomic formulas involving = using infix notation, i.e., a = b instead of =(a,b) . The equality predicate has special model-theoretic semantics,treated as explained in Section Model Theory for RIF's Basicfalse -- a formula that is always false.

• If φ is a well-formed condition Language .formula and ?V₁, ..., ?V_n are variables then Exists ?V₁ ... ?V_n ( φ ) is a well-formed condition formula.

Examples. ToWe illustrate the above definitions, we give severaldefinitions with the following examples. In addition to atomic, the examples also use another signature, term{ }. As we shall soon see, this signature is used in RIF-BLD.

Consider the term p(p(a) p(a b c))p ( p ( a ) p ( a b c ) ). If p has the (polymorphic) signature myPsigmysig{( iterm)⇒ iterm, ( i iterm term)⇒ iterm, ( i i iterm term term)⇒ iterm} and a, b, c each has the signature i { }term{ } then p(p(a) p(a b c))p ( p ( a ) p ( a b c ) ) is a well-formed term with signature i { }. If, for instance,term{ }. If instead p 'shad the signature were myPsig2mysig2{( i iterm term)⇒ iterm, ( i i iterm term term)⇒ iterm} then p(a)p ( p ( a ) p ( a b c ) ) would not have beenbe a well-formed term and the entire termsince then p ( a ) would alsonot be ill-formed. Here is another, fancier, signature forwell-formed (in this case, p under which the above termwould be well-formed (and againhave no arrow expression which allows p to take just one argument).

For a more complex example, let r have the signature i{ }): myPsig3mysig3{( iterm)⇒ boolatomic, ( bool iatomic term)⇒ iterm, ( i i iterm term term)⇒ iterm}. Then r ( r ( a ) r ( a b c ) ) is well-formed. The interesting twist here is that r ( a ) is a Boolean rather than an individual, but this is allowed by the arrow expression (atomic term)⇒ term, which is part of r's signature. If pr's signature were myPsig4mysig4{( iterm)⇒ boolatomic, ( bool iatomic term)⇒ boolatomic, ( i i iterm term term)⇒ iterm} instead, then p(p(a) p(a,b,c))r ( r ( a ) r ( a b c ) ) would have beenbe not only a well-formed term with signature bool { } and, therefore, it would have beenterm, but also a well-formed atomic formula.

An even more advanced example of a signatureusing signatures is when the right-hand side of an arrow expression is a signaturesomething other than iterm or boolatomic. For instance, let John, Mary, NewYork, and Boston have signatures i { };term{ }; flight and ancestorparent have signaturessignature h₂ {i ( i i{(term term)⇒ boolatomic}; and closure have signature hh₁{(h₂)⇒p₂}, where the signature p₂ is the name ofhas the signatureform p₂{( i iterm term)⇒ boolatomic}. Then closure(flight)(NewYork,Boston)flight ( NewYork Boston ), closure ( flight ) ( NewYork Boston ), parent ( John Mary ), and closure(ancestor)(John,Mary)closure ( parent ) ( John Mary ) would be well-formed formulas. Such formulas are allowed in languages like HiLog, which support predicate constructors like closure in ourthe above example.

More general formulas are constructed out of atomic formulas with2.1.1.3. Symbol Spaces

Throughout this document, the helpxsd: prefix stands for the XML Schema namespace URI http://www.w3.org/2001/XMLSchema#, the rdf: prefix stands for http://www.w3.org/1999/02/22-rdf-syntax-ns#, and rif: stands for the URI of logical connectives. RIF's Basic Condition Language definesthe following general well-formed formulasRIF namespace, http://www.w3.org/2007/rif#. If φ isSyntax such as xsd:string should be understood as a well-formed atomic formula then it is alsocompact uri -- a general well-formed formula. If are φ and ψ are general well-formed formulas then so is φ ∧ ψ. If are φ and ψ are general well-formed formulas then so is φ ∨ ψ. If φ is a well-formed general formula and V 1 , ..., V n are variables then ∃ V 1 ... V n φ is a general well-formed formula. Signatures in the RIF Basic Condition Language. RIF's basic condition language presents a much simpler picturemacro that expands to a concatenation of the usercharacter sequence denoted by restrictingthe setprefix xsd and the string string. In the next version of well-formed termsthis document we intend to introduce a specific coherent set of signatures. Namely,syntax for defining prefixes for compact URIs.

TODO: Define CURIs.

The signatureset of RIF's basic logic language contains the following signatures: i { } and bool { } For every integer arity n ≥ 0, there are signatures f n {( i ... i ) ⇒ i } and p n {( i ... i ) ⇒ bool } (there are n i 's inside the parentheses), which represent functionall constant symbols in RIF has a number of arity npredefined subsets, called symbol spaces, which are used to represent XML data types, data types defined in other W3C specifications, such as rdf:XMLLiteral, and predicate symbolsto distinguish other sets of arity n, respectively. In additionconstants. Constant symbols that belong to i and bool ,the symbols f nvarious symbol spaces have special presentation syntax and p n are reserved signature names in the RIF basic logic dialect. In this way, each constantsemantics.

Formally, a symbol can be either an individual,space is a predicatenamed subset of one particular arity, or a function symbolthe set of one particular arity.all variables are associated with signature i { }, so they can range only over individuals. The equality symbol, = , has signature p 2 {( i i ) ⇒ bool }. In this way, the equality predicate can compare onlyconstants, Const. The terms whose signature is i{ }; it cannot compare predicate names or function symbols.semantic aspects of symbol spaces. Throughout this document, the rif: prefix will stand for the XML Schema namespace URI http://www.w3.org/2001/XMLSchema and rif:spaces will standbe described in Section Model Theory for the URICondition Language of theRIF namespace, http://www.w3.org/2007/rifBLD.

The set of all constant symbols in RIFEach symbol space has an associated lexical space and a number of predefined subsets, called symbol spaces , which are used to represent XML data types, data types defined in other W3C specifications, such as rdf:XMLLiteral , and to distinguish other sets of constants.identifiers.

• The following primitive data types are supported: xsd:long ( http://www.w3.org/2001/XMLSchema#long ), xsd:string ( http://www.w3.org/2001/XMLSchema#string ), xsd:decimal ( http://www.w3.org/2001/XMLSchema#decimal ), xsd:time ( http://www.w3.org/2001/XMLSchema#time ), xsd:dateTime http://www.w3.org/2001/XMLSchema#dateTime ), and rdf:XMLLiteral ( http://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral ). Basic RIF logic defines two additional symbol spaces: rif:iri (for internationalized resource identifier or IRI ) and rif:local (for constant symbols that are not visible outsidelexical space of a particularsymbol space is a non-empty set of RIF formulas). Constant symbols that belong to the various symbol spaces will have special presentation syntax, and semantic structures will interpret them inUnicode character strings.

• An identifier of a special way. Insymbol space is an absolute IRI. The formal syntax, however, support forsame symbol spaces only requires usspace is allowed to state thathave more than one identifier (but different symbol spaces cannot share an identifier).

  To simplify the set Const of all constant symbols has subsets Const xsd:long , Constlanguage, this document will often use symbol space identifiers to refer to the actual symbol spaces (for instance, we may say "symbol space xsd:string , Const xsd:decimal , Const xsd:time , Const xsd:dateTime , Const rdf:XMLLiteral , Const rif:iri , and Const rif:local . These sets" instead of symbols are described"symbol space identified by xsd:string").

To refer to a constant in more detail later. 2.1.1.2. Abstract Syntaxa particular RIF symbol space, we defineuse the Abstract Syntax of BLD with (strictly) alternating syntactic class/property categories, i.e. in a "(fully) striped" manner. Sectionfollowing presentation Syntax will then proceed to a "stripe-skipped" or "unstriped" human-readable syntax as well as tosyntax:

     LITERAL^^SYMSPACE

where LITERAL is a (fully) striped XML syntax. TODO: Explain "fully striped." To compare two approaches at [ F2F7 ], we representUnicode string, called the abstract syntaxlexical part of the RIF Condition Language both in Abstract Syntax Notationsymbol, and in Abstract EBNF Syntax. 2.1.1.2.1. Abstract Syntax Notation The abstract syntax of the condition languageSYMSPACE is given in asn06 as follows: class CONDITION subclass And property formula : list of CONDITION subclass Or property formula : list of CONDITION subclass Exists property declare : list of Var property formula : CONDITION subclass ATOMIC class ATOMIC subclass Uniterm subclass Equal class Uniterm property op: Const property arg: list of TERM class Equal property side: list of TERM class TERM subclass Const property name: CONSTNAME property type: TYPENAME? subclass Var property name: VARNAME subclass Uniterm The lengthan identifier of the list of Var ofsymbol space in the declare property (role)form of the Exists class is assumed toan absolute IRI string. LITERAL must be 1 or more.an element in the multiplicitylexical space of the side propertysymbol space. For instance, 1.2^^xsd:decimal and 1^^xsd:decimal are legal symbols because 1.2 and 1 are members of the Equal classlexical space of the XML data type xsd:decimal. On the other hand, a+2^^xsd:decimal is assumed to be exactly 2. 2.1.1.2.2. Abstract EBNF Syntax We representnot a legal symbol, since a+2 is not part of the abstract syntaxlexical space of xsd:decimal.

RIF-compliant implementations must support the following symbol spaces. Rule sets that are exchanged through RIF Condition Language withcan use additional symbol spaces as explained below.

• xsd:long (http://www.w3.org/2001/XMLSchema#long).

• xsd:string (http://www.w3.org/2001/XMLSchema#string).

• xsd:integer (http://www.w3.org/2001/XMLSchema#integer).

• xsd:decimal (http://www.w3.org/2001/XMLSchema#decimal).

• xsd:time (http://www.w3.org/2001/XMLSchema#time).

• xsd:dateTime http://www.w3.org/2001/XMLSchema#dateTime).

The helplexical spaces of usual EBNF , employed here to define BLD in a fully striped normal form. In this Abstract EBNF Syntax ,the propertiesabove symbol spaces are named using idioms ofdefined in the form ' name ->' , e.g. 'formula ->'document XML Schema Part 2: Datatypes.

• CONDITION ::= 'And' '(' ('formula ->' CONDITION)* ')' | 'Or' '(' ('formula ->' CONDITION)* ')' | 'Exists' '(' ('declare ->' Var)+ 'formula ->' CONDITION ')' | ATOMIC ATOMIC ::= Uniterm | Equal Uniterm ::= 'Uniterm' '(' 'op ->' Const ('arg ->' TERM)* ')' Equal ::= 'Equal' '(' 'side ->' TERM 'side ->' TERM ')' TERM ::= 'Const'rdf:XMLLiteral ( '(' 'type ->' TYPENAME ')' )? '(' CONSTNAME ')' | 'Var' '(' VARNAME ')' | Unitermhttp://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral).

  This symbol space represents XML content. The above abstract syntax can be illustrated with a UML diagram, as shown below. Automatic transformation fromlexical space of rdf:XMLLiteral is defined in the document Resource Description Framework (RDF): Concepts and Abstract EBNFSyntax to UML can be implemented based on the earlier asn06-to-UML transformation.

• rif:text (for text strings with language tags attached).

  This symbol space represents text strings with a language tag attached. The central classlexical space of RIF, CONDITION ,rif:text is specified recursively through its subclasses and their parts.the Equal class has two side roles. Two pairsset of roles distinguish between the declare and formula parts of the Exists class, and between the operation ( op ) and arguments ( arg )all Unicode strings of the Uniterm class, where multiple arguments are subject to an ordered constraint (the natural "left-to-right" order): The syntactic classes are partitioned into classesform ...@LANG, i.e., strings that will not be visible in serializations (writtenend with @LANG where LANG is a language identifier as defined in all-uppercase letters) and classesIETF RFC 3066.

• rif:iri (for internationalized resource identifier or IRI).

  Constant symbols that willbelong to this symbol space are intended to be visibleused in instance markup (written witha leading uppercase letter only). The three classes Var , CONDITION , and ATOMIC will be required in the abstract syntax of Horn Rulesway similar to RDF resources. 2.1.1.3. Presentation SyntaxThe abstract syntaxlexical space consists of Section Abstract Syntax can be loweredall absolute IRIs as specified in RFC 3987; it is unrelated to a presentation syntax. The Presentation EBNF Syntax below, which lowersthe Abstract Syntax,XML primitive type anyURI. A rif:iri constant is used throughout this documentsupposed to be interpreted as a reference to explainone and illustratethe main ideas. This syntax is similarsame object regardless of the context in style to whatwhich that constant occurs.

• rif:local (for constant symbols that are not visible outside of a particular set of RIF formulas).

  Symbols in OWL is called the Abstract Syntax http://www.w3.org/TR/owl-semantics/syntax.html . Presentation EBNF Syntax. The human-oriented presentation syntax, describedthis symbol space are used locally in their respective rule sets. This EBNF (usual except for whitespace handling), is workmeans that occurrences of the same rif:local-constant in progress and under discussion. CONDITION ::= 'And' '(' CONDITION* ')' | 'Or' '(' CONDITION* ')' | 'Exists' Var+ '(' CONDITION ')' | ATOMIC ATOMIC ::= Uniterm | Equal Uniterm ::= Const '(' TERM* ')' Equal ::= TERM '=' TERM TERM ::= Const | Var | Uniterm Const ::= CONSTNAME | '"'CONSTNAME'"''^^'TYPENAME Var ::= '?'VARNAMEdifferent rule sets are viewed as unrelated distinct constants, but occurrences of the above is a standard syntax for a variantsame constant in the same rule set must refer to the same object. The lexical space of first-order logic.rif:local is the applicationsame as the lexical space of axsd:string.

Symbols with an ill-formed lexical part. RIF constant symbols that belong to one of the aforesaid RIF-supported symbol from Constspaces must be well-formed, i.e., their lexical part must belong to the lexical space associated with the symbol space. For instance, 123^^xsd:long has a sequence of terms is called Uniterm ("Universal term")correct lexical part, since it can be used123 belongs to playthe rolelexical space of a function term or an atomic formula depending onthe syntactic contextdata type xsd:long. In which the application occurs. The non-terminal ATOMIC stands for (positive) atomic formula , which can later be complementedcontrast, abc^^xsd:long is ill-formed, as it does not have a correct lexical part. A compliant RIF-BLD interpreter must reject ill-formed symbols.

Symbols with "negated atomic formula".undefined symbol spaces. RIF allows symbols of the 'Exists' formula is an "existential formula", which in Horn-like conditionsform LITERAL^^SYMSPACE where SYMSPACE is not one of the only quantified formula butpre-defined RIF symbol spaces. These are treated as "uninterpreted" constant symbols in later conditions may be complemented with "universal formula" ( Var+ denotesthe listRIF language and the lexical space of free variables in CONDITION ).such a symbol space is considered to be the 'And' formula defines conjunctionsset of conditions, and 'Or' denotes disjunctions. Finally, CONDITION assembles everything into what we call RIF conditions . RIFall Unicode strings. Dialects willthat extend these conditionsRIF-BLD might appropriate some of the symbol spaces, which are left undefined in various ways. Note that individuals, function symbols,RIF-BLD, and predicate symbols all belonggive them special semantics.

2.1.1.4. Signatures Used in the RIF-BLD Language

The condition language of RIF-BLD presents a much simpler picture to the sameuser by restricting the set of symbols ( Const ). This syntax is more general than what RIF's basic logic dialect actually permits. As explained in Section Formal Preliminarieswell-formed terms to a specific coherent set of signatures restricts this syntax to allow onlysignatures. Namely, the terms that are allowed in standard first-order logic.signature set of RIF-BLD contains the above Presentation EBNF Syntax, where TERM* is understood as TERM* ::= | TERM TERM*following signatures:

• term{ }, uses spaces to indicate Lisp-like whitespace ( SPACEatomic{ }, TABbi_atomic{ }, or NEWLINE ) character sequences inwhere bi_atomic<atomic.

  The defined language; these must consist of at least one whitespace character when used assignature term{ } represents the separator between adjacent TERM s, andcontext in which individual objects (but not atomic formulas) can consist of zero or more whitespace characters elsewhere. Where spaces are omitted fromappear. The Presentation EBNF Syntax,signature bi_atomic{ } represents atomic formulas for builtin predicates (such as between '?' and VARNAME in '?'VARNAMEfn:substring). Since bi_atomic<atomic, there must be no whitespace character in the defined language. Constant symbols can have two forms: CONSTNAMEbuiltin atomic formulas are also atomic formulas, but normally most atomic formulas are user-defined and "CONSTNAME"^^TYPENAME . The second form is more general. The first form is used as a shorthand for some symbol spaces, like long integers, decimals, local RIF constants, etc.they will have the precise syntaxsignature atomic rather than bi_atomic.

• For RIF constants is given in Section Primitive Data Types . At this point we do not commit to any particular vocabulary for the names of variables. These are assumed to be alphanumeric character sequences starting with a ?-sign. **** MK: should probably be more specific: Varsevery integer n ≥ 0, there are alphanums starting with a ? or something like ?'.....', if non-alphanum characterssignatures f_n{(term ... term) ⇒ term}, p_n{(term ... term) ⇒ atomic}, and bi_n{(term ... term) ⇒ bi_atomic} (in each case there are involved.n terms inside the loweringparentheses), which represent function symbols of arity n, (user-defined) predicate symbols of arity n, and n-ary builtin predicates, respectively. The abstract syntax to this presentation syntax can be done via automatic EBNF-to-EBNF mapping. The mapper, abs2con4g (" abs tract to con crete for g rammar"), uses a TokenTable parameter specifying how to map certain abstract classes,symbols f_n p_n, and bi_n are reserved signature names in prefix notation, to operators,RIF-BLD.

• A symbol in infixConst can have exactly one signature, f_n, p_n, or prefix notation. This table is given inbi_n, where n ≥ 0. It cannot have the formsignature atomic or bi_atomic (only terms can have such signatures, not symbols). Thus, in RIF-BLD each constant symbol can be either an individual, a predicate of binary class2token facts, accessed viaone particular arity, a lookup function. The main mapper is given in the formbuiltin of (left-to-right oriented) equations defining abs2con4g asone particular arity, or a binaryfunction withsymbol of one particular arity -- it is not possible for the abstract syntax as first argument,same symbol to play more than one role.

• The table as second argument,constant symbols that correspond to XML Schema data types all have the signature term in RIF-BLD. The symbols of type rif:iri and rif:local can have the presentation syntax as returned value. class2token('Equal','=') class2token('type','^^') class2token('Var','?') abs2con4g(?Production1 ... ?ProductionN, ?TokenTable) = abs2con4g(?Production1, ?TokenTable) ... abs2con4g(?ProductionN, ?TokenTable) abs2con4g(?LeftSymbol ::= ?RightExpression, ?TokenTable) = ?LeftSymbol ::= abs2con4g(?RightExpression, ?TokenTable) abs2con4g('And' '(' ('formula ->' CONDITION)* ')' | 'Or' '(' ('formula ->' CONDITION)* ')' | 'Exists' '(' ('declare ->' Var)+ 'formula ->' CONDITION ')' | ATOMIC, ?TokenTable) = 'And' '(' CONDITION* ')' | 'Or' '(' CONDITION* ')' | 'Exists' Var+ '(' CONDITION ')' | ATOMIC abs2con4g(Uniterm | Equal, ?TokenTable)following signatures in RIF-BLD: term, f_n, p_n, or bi_n, for n = Uniterm | Equal abs2con4g('Uniterm' '(' 'op ->' Const ('arg ->' TERM)* ')', ?TokenTable)0,1,....

• All variables are associated with signature term{ }, so they can range only over individuals.

• RIF-BLD also reserves a special constant, = Const '(' TERM* ')' abs2con4g('Equal' '(' 'side ->' TERM 'side ->' TERM ')', ?TokenTable), to represent the predicate of equality. The equality symbol, =, has signature p₂{(term lookup('Equal',?TokenTable)term abs2con4g(Const | Var | Uniterm, ?TokenTable) = Const | Var | Uniterm abs2con4g('Const' ('(' 'type ->' TYPENAME ')')? '(' CONSTNAME ')', ?TokenTable) = CONSTNAME(lookup('type',?TokenTable)TYPENAME)? abs2con4g('Var' '(' VARNAME ')', ?TokenTable) = lookup('Var',?TokenTable)VARNAME Note) ⇒ atomic}. This means that variables inthe RIF Condition Languageequality predicate can be free or quantified . All quantificationcompare only the terms whose signature is explicit. All variables introduced by quantification must also occur interm; it cannot compare predicate names or function symbols.

  The quantified formula. Initially, only existential quantificationequality predicate is used. Universal quantification will be introduced later.said to belong to the symbol space rif:local so, strictly speaking, we should write it as =^^rif:local. However, we adoptwill usually omit the usual scoping rulessymbol space, for quantifiers from first-order logic. Variables that are not explicitly quantified are free . Free variables arise because CONDITION can occur in an if partreadability.

  For convenience we will write equations using infix notation, i.e., a = b instead of a rule. When this happens,=(a,b). The free variablesequality predicate has special model-theoretic semantics, as explained in aSection Model Theory for Condition formula are precisely those variablesLanguage of RIF BLD.

  Note that also occuralthough = has a special semantics, it is not a builtin predicate. In the then partparticular, terms of the rule. We shall see in Section Horn Rules that such variables are quantified universally outside ofform a = b have the rule,signature atomic and the scope of such quantificationnot bi_atomic.

RIF-BLD requires no extra syntax for declaring signatures, since signatures can be inferred. Indeed, RIF-BLD requires that each symbol is associated with a unique signature. Therefore, the entire rule. For instance,signature can be determined from the variable ?Ycontext in which the first RIF condition of Example 1 is quantified, existentially, but ?Xsymbol is free. However, when this condition occurs in theused. If part of the second rule in Example 1, then this variablea symbol is quantified universally outside of the rule. (The precise syntax for RIF rules will be given in Section Horn Rules .) Example 1 (A RIF conditionused in and outside ofmore than one context, the parser should treat it as a rule) RIF condition: Exists ?Y (condition(?X ?Y)) RIF Horn rule: Forall ?X (then-part(?X) :- Exists ?Y (condition(?X ?Y))) When RIF conditionssyntax error. If no errors are used as queries, their free variables carry answer bindings back to the caller. 2.1.2. Symbol Spacesfound, all uniterms and Primitive Data Types Following N-Triples , we will use the following presentation syntax to specify the constant symbols that belongatomic formulas are guaranteed to be well-formed. As a symbol space label : "literal"^^label For instance, "123"^^xsd:long is a symbol that belongs toconsequence, signatures are not part of the symbol space xsd:longRIF-BLD language and term, "2007-11-23T03:55:44-02:30"^^xsd:dateTime is a symbol in symbol space xsd:dateTimeatomic, and "ftp://example.com/foobar"^^rif:iri is a symbol that belongsbi_atomic are not reserved keywords.

Builtin predicates are not subject to the symbol space rif:iri .above signature inference rule. The partsignatures of such a symbol that occurs insidethe double quotes is called the lexical form of the symbol. The surrounding double quotesbuiltin predicates are not part of the literal. If a double quote is included as part of a literal, it must be escapeddefined by List_of_functions_and_operators. In particular, all symbols with the backslash. Some data typeshttp://www.w3.org/2005/xpath-functions# prefix are considered to be builtins and have shorthand notation in whichsignatures of the ^^label part can be omitted (see below). A symbol spaceform bi_n{... ⇒ bi_atomic}.

In dialects that extend RIF-BLD, signature inference may not always be possible. We expect that most dialects will use signature inference and RIF hasdoes not define any special sublanguage for signatures. However, signature inference may not always be possible or desirable in some dialects. In these cases, we expect those dialects to introduce their own primitives for defining signatures.

2.1.1.5. EBNF for the following components: A non-empty setPresentation Syntax of character strings calledthe lexical space ofRIF-BLD Condition Language

The symbol space.overall structure of the lexical space for a type, D , determines which character strings are allowed as value in a symbol like " value " D . For instance, "1.2"^^xsd:decimal and "1"^^xsd:decimal are two legal symbols because 1.2 and 1 are legalsyntax used in the lexical space of the XML datatype xsd:decimal .RIF-BLD condition sublanguage is depicted on the other hand, "a+2"^^xsd:decimal is not a legal symbol, since a+2following diagram.

The central syntactic class of RIF, CONDITION, is not partspecified recursively through its subclasses and their parts. The Equal class has two side roles. Two pairs of roles distinguish between the lexical spacedeclare and formula parts of the XML datatype xsd:decimal . An absolute IRI that identifiesExists class, and between the symbol space. A constant symboloperation (op) and arguments (arg) of the form "xyz"^^label is well-formed if its lexical form, xyz belongsUniterm class, where multiple arguments are subject to an ordered constraint (the natural "left-to-right" order).

The lexical space associated with the symbol space label . In addition the semantics of a symbol space defines A non-empty set called the value space of the data type; and A mapping from the lexical space of the data type to its value space. These two componentssyntactic classes are partitioned into classes that will not be explainedvisible in Section Model Theory for RIF's Basic Condition Language . We would like to point out, however, that symbol spacesserializations (written in RIF include spaces, such as xsd:long , whose value space is fixed as well as spaces like rif:iriall-uppercase letters) and rif:local whose value spaces are not fixed. Weclasses that will refer to the former as primitive data types . A number of primitive typesbe visible in RIF are based oninstance markup (written with a leading uppercase letter only).

The XML Schema data types,three classes Var, CONDITION, and their namesATOMIC are references to the corresponding XML Schema types.used in this version ofthe RIF BLD document,syntax of Horn Rules.

We define the following symbol spaces, where the prefix xsd refers tonow give an EBNF for the XML Schema URI andRIF presentation syntax. This syntax is somewhat abstract in nature. In particular, it does not address the prefixconcrete details of how constants and variables are represented. For instance, it ignores the RIF language. The syntaxissues that have to do with delimiters, such as xsd:long should be understoodwhite spaces and escape symbols. Instead, white space is informally used as a compact uri , i.e., a macro, which expandsdelimiter. For instance, TERM* is to a concatenation of the character sequence denoted by the prefix xsd and the string longbe understood as TERM* ::= | TERM TERM*. In the next version ofThis document we will introduceis done on purpose, since RIF's presentation syntax is intended to be used for specifying semantics and to illustrate the main RIF concepts through examples. It is not intended as a concrete syntax for defining prefixesa rule language. RIF defines a concrete syntax only for compact URIsexchanging rules, and will also expand onthat syntax is XML-based.

  CONDITION   ::= 'And' ' ( ' CONDITION* ' ) ' |
                  'Or' ' ( ' CONDITION* ' ) ' |
                  'Exists ' Var+ ' ( ' CONDITION ' ) ' |
                  ATOMIC
  ATOMIC      ::= Uniterm | Equal
  Uniterm     ::= Const ' ( ' TERM* ' ) '
  Equal       ::= TERM ' = ' TERM
  TERM        ::= Const | Var | Uniterm
  Const       ::= LITERAL '^^' SYMSPACE
  Var         ::= '?' VARNAME

The above is a standard syntax for a variant of first-order logic. The symbols that can be used to denote RIF's primitive data types. xsd:long . Thisapplication of a constant (Const) symbol space correspondsto the XML data type xsd:long . Example: "123"^^xsd:long . Long integers also havea short notation, which does not require the "..."^^xsd:long wrapper. That is, long integerssequence of terms is called a Uniterm (Universal term); it can be written as constants fromplay the lexical spacerole of xsd:long , buta term or an atomic formula depending on the surrounding double quotes andsyntactic context in which the type label ^^xsd:long can be omitted. Example: 123 . xsd:decimal . This corresponds toapplication occurs. The XML data type xsd:decimalnon-terminal ATOMIC stands for atomic formula. Example: "123.45"^^xsd:decimal . Decimals also have an alternative short notation, which does not requireThe "..."^^xsd:decimal wrapper. That is, decimals can be written as constants fromExists formula, where Var+ stands for the lexical spacelist of xsd:decimalvariables that are free in CONDITION, but the surrounding double quotes and the type label ^^xsd:decimal can be omitted. Example: 123.45is an existential formula. The type xsd:decimalIt is a supertypethe only kind of xsd:long . xsd:string . This corresponds toquantified formulas in RIF-BLD, but other dialects may add universal quantification. The XML data type xsd:string . Example: "a string"^^xsd:stringAnd formula defines conjunctions of conditions, and 'Or' denotes disjunctions. Finally, CONDITION assembles everything into what we earlier called RIF condition formulas.

Double quotesNote that appear inside strings are escaped with a backslashindividuals, function symbols, and a backslash that is supposedpredicate symbols all belong to appear inthe string must be escaped with another backslash. xsd:timesame set of symbols Const. This correspondssyntax is more general than what RIF-BLD actually permits. As explained in Section Symbols and Signatures a set of signatures further restricts this syntax to allow only the XML data type xsd:time . Example: "18:33:44.2345"^^xsd:time . xsd:dateTime . This type correspondsstandard first-order logic terms.

RIF-BLD presentation syntax does not commit to any particular vocabulary for the XML data type xsd:dateTime . Example: "2007-03-12T21:22:33.44-01:30"^^xsd:dateTime . rdf:XMLLiteral . This type's lexical space isnames of variables or for the literals used to represent certain XML documents, as describedin Resource Description Framework (RDF): Concepts and Abstract Syntax . rif:iri . Symbolsconstant symbols. In this symbol spacethe examples, variables are denoted by Unicode character sequences beginning with a ?-sign. Constant symbols have the form "XYZ"^^rif:iriform: LITERAL^^SYMSPACE, where XYZSYMSPACE is an absoluteIRI as specified in RFC 3987 . rif:local . Symbols instring that identifies the symbol space haveof the form "XYZ"^^rif:local , where XYZconstant and LITERAL is any string of characters (provided that each occurrence of " and of \ in sucha Unicode string is escaped with a backslash). Thus,from the lexical space of rif:local is the same asthat symbol space.

In the lexical spacecondition language of xsd:stringRIF-BLD, a variable can be free or quantified. Local symbolsAll quantification is explicit and the variables introduced by quantification must also have an alternative short notation. Example: 'a local symbol' .occur in this notation, single quotes and backslashesthe quantified formula. Variables that occur inside such stringsare escaped with backslashes. TODO: Define CURIs. Other XML data types thatnot explicitly quantified are likely to be incorporated in RIF include xsd:double , xsd:date , and a type for temporal duration . At present, the partial order on the above primitive data types is imposed by the XML Schema hierarchy, so the only subtype relationship is between xsd:long and xsd:decimalfree.

This may be extended as more typesConditions with free variables are added. The symbol space rif:iri is intended to beused as queries and also in a way similar to RDF resources .the value spaceif part of a rule. In the symbol space rif:iri can be any set and nolatter case, the free variables in a priori equalities amongcondition formula must also occur in the membersthen part of the type rif:irirule. We shall see in Section Horn Rules that such variables are assumed. This domain is not the same as the value spacequantified universally outside of the XML primitive type anyURI .rule, and the symbol space rif:localscope of such quantification is usedthe entire rule. For constant symbols (including predicate and function symbols) that are local toinstance, the various sets ofvariable ?Y in the first RIF formulas. They are not visible outsidecondition of the rule set in which these constants occur (except, possibly, when such a constantExample 1 is equated to a constant of type rif:iri ). TODO. We will need to definequantified, existentially, but ?X is free. However, when this condition occurs in the notionif part of the second rule set more precisely. For instance, what is the rule setin which a particular rule occurs? Will we have #include statements? Import? AllExample 1, then this has to be hashed out. The constant symbols that correspond to XML Schema data types all havevariable is quantified universally outside of the signature i { }rule. (The precise syntax for RIF rules is given in Section Horn Rules.)

Example 1 (A RIF condition in  RIF's basic logic dialect. The symbols of type rif:iriand  rif:local can have any signature allowed by the basicoutside of a rule)

 RIF  logic: i , f n , or p n , for n = 0,1,.... Symbols with ill-formed lexical part.condition:
                        Exists ?Y ( condition ( ?X ?Y ) ) 

 RIF  constant symbols that belong toHorn rule:
        Forall ?X ( then_part ( ?X ) :-  Exists ?Y ( condition ( ?X ?Y ) ) )

2.1.1.6. XML Syntax

EDITORS' NOTE: The XML syntax for BLD presented here is one of the RIF-supported symbol spaces must be well-formed, i.e., their lexical form must belong to the lexical space associated withproposals the symbol space. For instance, "123"^^xsd:long has a correct lexical form, since 123 belongsWorking Group is considering. It is presented here to get feedback on this strawman and to give readers an idea for the lexical spacekind of information that will be presented in this section.

The data type xsd:long .XML serialization for RIF-BLD presentation syntax given in contrast, "abc"^^xsd:long is ill-formed, as it does not have a correct lexical form. A compliant RIF interpreter must reject such symbols. Symbols with undefined symbol spaces. RIF allows symbols of the form "..."^^label where label is not one of the previously defined standard symbol spaces (such as xsd:long , rif:local , etc.). These are treated as uninterpreted constant symbols in the RIF language. For instance, "abc"^^cde is such an uninterpreted symbol. Dialects that extend the basic RIF logic dialect might appropriate some of the symbol spaces, which are undefined in the basic RIF dialect, and give them special semantics. 2.1.3. XML serialization EDITOR'S NOTE: The XML syntax for BLD presented here is one of the proposals the Working Group is considering. It is presented here to get feedback on this strawman and to give readers an idea for the kind of information that will be presented in this section. The XML serialization for RIF abstract syntax presented in Section Abstract Syntaxthis section is fully striped. Positional information is optionally exploited only for the arg role elements. For example, role elements (declare and formula) are explicit within the Exists element. Following the examples of Java and RDF, we use capitalized names for class elements and names that start with lowercase for role elements.

The all-uppercase classes in the abstractpresentation syntax, such as CONDITION, become XML entities. They act like macros and are not visible in instance markup. The other classes as well as non-terminals and symbols (such as Exists or =) become XML elements with optional attributes, as shown below (see also Appendix Specification ).below.

- And     (conjunction)
- Or      (disjunction)
- Exists  (quantified formula for 'Exists', containing declare and formula roles)
- declare (declare role, containing a Var)
- formula (formula role, containing a CONDITION formula)
- Uniterm (atomic or function-expression formula)
- op      (operation role)
- arg     (argument  role, positional/non-positional without/with optional 'index' attribute)role)
- Equal   (prefix version of term equation '=')
- side    (left-hand and right-hand side role)
- Const   (predicate symbol, function symbol, or individual, with optional 'type' attribute)
- Var     (logic variable)

For the XML Schema Definition (XSD) of the RIF-BLD condition language see Appendix Specification.

The XML syntax for symbol spaces utilizes the type attribute associated with XML term elements such as Const. For instance, a literal in the xsd:dateTime data type can be represented as <Const type="xsd:dateTime">2007-11-23T03:55:44-02:30</Const>.

The following example illustrates XML serialization of RIF conditions.

Example 2 (A RIF condition and its XML serialization):
  We use the prefix bks as an abbreviation for http://example.com/books#
  and curr for http://example.com/currencies#

a. RIF  condition:condition

  And ( Exists ?Buyer  (purchase(?Buyer( purchase^^rif:local ( ?Buyer
                                              ?Seller
                                               book(?Author "http://example.com/books#LeRif"^^rif:iri) "http://example.com/currencies#USD"^^rif:iri(49)))book^^rif:local ( ?Author bks:LeRif^^rif:iri )
                                              curr:USD^^rif:iri ( 49^^xsd:integer ) )
        ?Seller=?Author )

b. XML  serialization: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">http://example.com/books#LeRif</Const></arg>type="rif:iri">bks:LeRif</Const></arg>
              </Uniterm>
            </arg>
            <arg>
              <Uniterm>
                <op><Const  type="rif:iri">http://example.com/currencies#USD</Const></op>type="rif:iri">curr:USD</Const></op>
                <arg><Const  type="xsd:long">49</Const></arg>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>

2.1.3.1. Specifying Signatures in RIF Dialects DaveR: Not clear what's2.1.1.7. Translation Between the value of giving an informal example instance XML document for signature specifications here. Either formally definePresentation and the XML syntax for signatures or dropSyntaxes

The example. We will now explain how signatures are defined intranslation between the Basic Condition Languagepresentation syntax and its extensions. In RIF's basic Logic dialect, there is no need to declare signatures, since they can be inferred. Indeed,the basic logic dialect requires that each symbolXML syntax is associated with a unique signature. Therefore, the signature can be determinedgiven by the context in which the symbol is used. Ifa symbol is used in more than one context, the parser should deem ittable as afollows.

Presentation Syntax	error. In dialects that extend RIF's Basic Condition Language, signature inference of the above kind is not possible, in general, and advanced signature inference might not always be appropriate even when it is possible. For this reason, we introduce the attribute sig for theXML elements ConstSyntax
And Var( conjunct1 . The value of such an attribute is supposed to be the signature. . 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>
predfunc ( argument1 . . . argumentn )	<Uniterm> <op>predfunc</op> <arg>argument1</arg> . . . <arg> argumentn</arg> </Uniterm>
left = right	<Equal> <side>left</side> <side>right</side> </Equal>
name^^space	<Const type="space">name</Const>
?name	<Var>name</Var>

2.1.2. Model Theory for Condition Language of RIF BLD

The corresponding symbol. For instance,first step in the above example, purchase wasdefining a 4-ary predicate, so it could be specified as <Const sig="p4">purchase</Const> . Since variables in the basic conditionmodel-theoretic semantics for a logic-based language always haveis to define the signature inotion of a semantic structure, we could write <Var sig="i">Author</Var>also known as an interpretation. The sig attribute is optional, and its value can be inferred for the basic language. For instance, in our example, the values p4 and i for the attribute sig could be inferred from the usage of the symbols purchase and Author . Dialects that extend the basic logic dialect can adopt their own rules for omitting this attribute and for inferring its values. The basic language does not need any special syntax for defining signatures -- all signature names are already defined: bool , i , f0 , f1 , p0 , p1 , etc. The dialects, however, will need a special sublanguage for defining signatures. The signature mysig{ (s1 s2 s3) -> bool (s i) -> i } can, for example, be defined using the following XML excerpt: <Signature signame="mysig"> <element> <Sigexpr sighead="bool"> s1 s2 s3 </Sigexpr> </element> <element> <Sigexpr sighead="i"> s i </Sigexpr> </element> </Signature> 2.1.4. Model Theory for RIF's Basic Condition Language The first step in defining a model-theoretic semantics for a logic-based language is to define the notion of a semantic structure , also known as an interpretation . (See end note on(See end note on the rationale.) In this section we define basic semantic structures. This definition will be extended in Extension of Semantic Structures for Frames when we introduce frame syntax.

2.1.2.1. Basic semantic structures. A basicstructures

Semantic structure , I , isstructures are used to assign a tuple of the form < D , I C , I V , I F , I R >, which determines thetruth value of every formula, as explained below.to each formula. Currently, by formula we mean anything produced by the CONDITION production in the presentation EBNFsyntax. Later on, formulas will also include rules. Other dialects might extend thisWe first define the notion even further.of a truth value formally and then introduce semantic structures. Next we give the semantics to symbol spaces and, finally, define truth values of formulas with respect to semantic structures.

Truth values. The set of truth values is denoted by TV. For RIF's basic logic dialect,RIF-BLD, TV includes only two values, t (true) and f (false). (See end note on truth values.)

The setIn RIF, TV has a total or partial order, called the truth order ; it is, and denoted with <_t. In the basic RIF logic,RIF-BLD, f <_t t, and it is a total order. (See end note on ordering truth values.)

To define howSemantic structures determine the truth values of RIF formulas, we introducestructures. A basic semantic structure, I, is a tuple of the following sets:form <D -,I_C, I_V, I_F, I_R>.

Here D is a non-empty set of elements called the domain of interpretation of I ,. We will continue to use Const -to refer to the set of individuals, predicate names,all constant symbols and function symbols,Var -to refer to the set of variables.all variable symbols.

The mappings that constitute an interpretation,other components of I ,are mappings defined as follows:

• I_C from Const to elements of D

• I_V from Var to elements of D

• I_F from Const to functions from D* into D (here D* is a set of all tuples of any length over the domain D)

• I_R from Const to partial truth-valued mappings D* → TV

  ItThe equality predicate, =, is convenientalways interpreted in the same way by all semantic structures: I_R(=) is a truth-valued mapping such as I_R(=)(<a,a>) = t for every a ∈ D; it maps other tuples of elements of D to f.

We also define a more generalthe following mapping, I, based on the mappings I_C, I_V, I F ,and I _RF:

• I(k) = I_C (k)(k), if k is a symbol in Const

• I(?v) = I_V (?v)(?v), if ?v is a variable in Var

• I (f(t(f ( t₁ ... t_n )) = I_F(f)(I(t₁),...,I(t_n))

Truth valuation for formulas. Observe thatSemantics of symbol spaces. Symbol spaces affect the notiondomain of signaturesI and the mapping I_C as follows. First, some symbol spaces, called primitive data types, have a value space, denoted VS_symsp, and a mapping from Section Formal Preliminaries is used onlythe lexical space to constrainthe syntaxVS_symsp, denoted L_symsp, where symsp is an identifier for the symbol space.

The value space and does not appear inthe definitionlexical-to-value-space mapping are defined as part of the semantic structure. This is because when we define truth valuationsdata type definition and do not depend on I. For formulas, below, all formulas are assumed to be well-formed. Truth valuationevery primitive datatype symsp it must hold that:

• VS_symsp ⊆ D; and

• For well-formed formulaseach constant lit^^symsp in RIF's basic condition language is determined usingthe following function, denoted I Truth : Atomic formulas: I Truth (r(t 1 ... t n )) = I R (r)( I (t 1 ),..., I (t n )) Equality: I Truth (t 1 =t 2 ) = t iff I (t 1 ) = I (t 2 ); I Truth (t 1 =t 2 ) = f otherwise. Conjunction:symbol space symsp, I _{Truth (And(c 1 ...C} n )) = min t( I Truth (c 1 ),..., I Truth (c n )), where min t is minimum with respect to the truth order. Disjunction: I Truth (Or(c 1 ... c n ))lit^^symsp) = max tL_symsp( I Truth (c 1 ),..., I Truth (c n )), where max t is maximum with respectlit).

  That is, when restricted to the truth order. Quantification: I Truth ( Exists ?v 1 ... ?v n (c)) = max t ( I * Truth ( c )), where max t is taken over all interpretations I * of the form < Da symbol space, symsp, I_C , I * V , I F , I R >, where the mapping I * V has the same value as I V on all variables except, possibly, onmust map the variables ?v 1 ,..., ?v ncorresponding constants according to L_symsp.

Notice that the mapping I Truth is uniquely determined by the four mapping comprising I and, therefore, itRIF-BLD does not need to be listed explicitly.impose restrictions on the interpretation of symbol spaces. We now explain howconstants (the mapping I_C) in symbol spaces which are integrated into the semanticsnot primitive datatypes. Other dialects may do so. An example of such a restriction is that no constant in a particular symbol space may be mapped to an element in the basic RIF logic. As mentioned earlier,value space of any XML data type.

The above semantics is not limited to any particular set of asymbol spaces or primitive data types. Any symbol space defines an associatedis covered as long as its lexical space is well-defined, and any data type is acceptable as long as its value space and a mapping fromthe lexical space tolexical-to-value mapping are known. For the primitive data types that are currently supported by RIF, their value space.spaces and the value space may be constrained in various ways or it can be completely fixed.lexical-to-value-space mappings are defined as follows:

• For instance,XML data types (xsd:long, xsd:integer, xsd:decimal, xsd:string, xsd:time, and xsd:dateTime), these are defined in the XML Schema Part 2: Datatypes specification defines a concretespecification.

• The value space for each XML data type, includingthe primitive data types such as xsd:decimaltype rdf:XMLLiteral is defined in Resource Description Framework (RDF): Concepts and Abstract Syntax.

• The value space of rif:text is the set of all pairs of the form (string, lang), where string is a Unicode character sequence and lang is a lowercase Unicode character sequence which areis a natural language identifier as defined by RFC 3066. The lexical-to-value mapping of text, L,,text,,, maps each symbol string@lang in the lexical space of interestrif:text to RIF.(string, lower-case(lang)), where lower-case(lang) is lang written in all-lowercase letters.

  The value space is different fromand the lexical-to-value mapping for rif:text defined here are compatible with RDF's semantics for strings with named tags.

The value space of a data type should not be confused with the lexical space. Lexical space refers tospaces define the syntax of the constant symbols that belong to a particularthe various primitive data type. Fortypes. In contrast, value spaces define the meaning of the constants in data types. The lexical and the value spaces are often not even isomorphic. For instance, "1.2"^^xsd:decimal1.2^^xsd:decimal and "1.20"^^xsd:decimal1.20^^xsd:decimal are two legal constants in RIF because 1.2 and 1.20 belong to the lexical space of xsd:decimal. However, these two constants are interpreted by the same element of the value space of the xsd:decimal type. Other symbol spaces may have their value spaces constrained in some ways, but not fixed. For instance, the value space of rif:iriTherefore, 1.2^^xsd:decimal = 1.20^^xsd:decimal is defined below as the entire domain of interpretation. This means that this value space cannot be an arbitrary subset of that domain. Some symbol spaces may have their value spaces restricted in other ways.a RIF tautology. Likewise, RIF semantics for data types implies certain inequalities. For instance, abc^^xsd:string ≠ abcd^^xsd:string is a value space may be required to be disjoint fromtautology, since I_C must map these two constants into distinct elements in the value space of xsd:string. On the XML data types. Formally, each data type comes with a value space, denoted by D type (for instance, D xsd:decimal ), andother hand, abc^^rif:local ≠ abcd^^rif:local is not a mapping,tautology in RIF, since I_C : Const type → D type . We require that D type ⊆ D for each XML data type, where Const type denotesis not restricted over the setlexical space of rif:local and these two constants incan be mapped to the same element in D in some semantic structures and to different elements in others.

Semantics of undefined symbol spaces. Section Symbol space type . The valueSpaces andaddressed the corresponding mappings forsyntactic aspects of the XML data typestreatment of "unknown" symbol spaces, i.e., symbol spaces that are not defined by the XML Schema Part 2: DatatypesRIF specification. In some cases,It defined the XML Schema specification defineslexical space of those symbols as the subdomains D s and D t for different XML primitive types s and t as being disjoint or as subsetsset of each other. For instance, theall Unicode strings. Semantically, unknown symbol spaces are treated as follows. First, they are not assigned any value space of xsd:long is definedspace. Thus, such symbol spaces are not considered to be a subset of xsd:decimal . The requirements imposedprimitive data types by the XML Schema specificationRIF even though they may have interesting consequences for the mappings from the lexical space to the value space. For instance,be viewed as data types by some concrete rule languages that use RIF for xsd:decimalexchange. Second, RIF does not impose any restrictions on the mapping I_C : Const xsd:decimal → D xsd:decimal is such that, for instance, I C ( "1.2"^^xsd:decimal ) = I C ( "1.20"^^xsd:decimal ) in every semantic structure. So, it follows that "1.2"^^xsd:decimal = "1.20"^^xsd:decimal is a RIF tautology.over the semanticsunknown symbol spaces.

Truth valuation of XML also implies some inequalities. For instance, since distinct strings are different in the value space forformulas. Observe that the xsd:string data type, something like "abc"^^xsd:string ≠ "abcd"^^xsd:string is a tautology, since itnotion of signatures from Section Symbols and Signatures is true in all RIF semantic structures. Onused only to constrain the other hand, "abc"^^rif:iri ≠ "abcd"^^rif:iri issyntax and does not a tautology in RIF, since it is possibleappear in somethe definition of the semantic structures (but notstructure. This is because when we define truth valuations for formulas, below, all such structures) that,formulas are assumed to be well-formed.

Truth valuation for example,well-formed formulas in RIF-BLD is determined using the following function, denoted I _CTruth:

• Atomic formulas: I_Truth(r ( "abc"^^rif:iri )t₁ ... t_n )) = I _{C ( "abcd"^^rif:iri ). The value space forR}(r)(I(t₁),...,I(t_n))

  Note that the RDF data type rdf:XMLLiteraldefinition of I_R(=) implies that I_Truth(t₁ = t₂) = t iff I(t₁) = I(t₂); I_Truth(t₁=t₂) = f otherwise.

• Conjunction: I_Truth(And ( c₁ ... c_n )) = min_t(I_Truth(c₁),...,I_Truth(c_n)), where min_t is defined in Resource Description Framework (RDF): Concepts and Abstract Syntax . For the symbol space rif:iri ,minimum with respect to the corresponding mapping istruth order.

• Disjunction: I_Truth(Or ( c _{: Const rif:iri → D , i.e., D rif:iri1} ... c_n )) = D . That is, the interpretation allowsmax_t(I_Truth(c₁),...,I_Truth(c_n)), where max_t is maximum with respect to map any IRI into any value in the domain of the semantic structure. The value space ofthe local RIF symbolstruth order.

• Quantification: I_Truth(Exists ?v₁ ... ?v_n ( c )) = max_t(I*_Truth(c)), where max_t is alsotaken over all interpretations I* of the entire domainform <D and,I_C, I*_V, I_F, I_R>, where the correspondingmapping looks as follows:I C : Const rif:local → D . Thus, local constants can denote any element of*_V has the domain of discourse, including integers, strings, etc.same value as I_V on all variables except, possibly, on the variables ?v₁,...,?v_n.

Notice that the mapping I_Truth is uniquely determined by the four mappings comprising I and, therefore, it does not need to be listed explicitly.