### The Semantics of RIF-BLD as a Specialization of RIF-FLD

This section defines the precise relationship between the semantics of RIF-BLD and the semantic framework of RIF-FLD. The remaining sections describe the semantics of RIF-BLD without referring to the general framework -- except for Primitive Data Types whose definition is not duplicated here.

The semantics of the RIF Basic Logic Dialect is defined by specialization from the semantics of the [:FLD/Semantics:Semantic Framework 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 need to specialize for RIF-BLD.

Recall that the * semantics of a dialect* is derived from these notions by specializing the following parameters.

*The effect of the syntax*.- RIF-BLD does not support negation. This is the only obvious simplification with respect to RIF-FLD as far as the semantics is concerned.

*Truth values*.The set

of truth values in RIF-BLD consists of just two values,**TV****t**and**f**such that**f**<_{t}**t**. Clearly, <_{t}is a total order here.

*Data types*.RIF-BLD supports all the data types listed in Section Primitive Data Types of RIF-FLD:

`xsd:long``xsd:integer``xsd:decimal``xsd:string``xsd:time``xsd:dateTime``rdf:XMLLiteral``rif:text`

*Logical entailment*.- Recall that logical entailment in RIF-FLD is defined with respect to an unspecified set of intended semantic structures and that dialects of RIF must make this notion concrete. For RIF-BLD, this set is defined in one of the two following equivalent ways:
- as a set of all models; or
- as the unique minimal model.

These two definitions are equivalent for entailment of RIF-BLD conditions by RIF-BLD rulesets, since all rules in RIF-BLD are Horn -- it is a classical result of Van Emden and Kowalski [vEK76].

- Recall that logical entailment in RIF-FLD is defined with respect to an unspecified set of intended semantic structures and that dialects of RIF must make this notion concrete. For RIF-BLD, this set is defined in one of the two following equivalent ways:

### Truth Values

The set * TV* of truth values in RIF-BLD consists of just two values,

**t**and

**f**. This set has a total order, called

*, such that*

**truth order****f**<

_{t}

**t**.

### Semantic Structures

A * semantic structure*,

*, is a tuple of the form <*

**I***,*

**TV***,*

**DTS***,*

**D**

**I**_{C},

**I**_{V},

**I**_{F},

**I**_{frame},

**I**_{SF},

**I**_{sub},

**I**_{isa},

**I**_{=},

**I**_{Truth}>. Here

*is a non-empty set of elements called the*

**D***of*

**domain***, and there is a proper subset,*

**I**

**D**_{ind}⊂

*, which is used to interpret individuals. We use*

**D**`Const`to refer to the set of all constant symbols and

`Var`to refer to the set of all variable symbols.

*denotes the set of truth values that the semantic structure uses and*

**TV***is the set of primitive data types used in*

**DTS***(please refer to Section Primitive Data Types of RIF-FLD for the semantics of data types).*

**I**The other components of * I* are

*total*mappings defined as follows:

**I**_{C}maps`Const`to elements of.**D**- This mapping interprets constant symbols.
If a constant,

`c`∈`Const`, occurs in the position of an*individual*then it is required that**I**_{C}(`c`) ∈**D**_{ind}.

- This mapping interprets constant symbols.
**I**_{V}maps`Var`to elements of**D**_{ind}.- This mapping interprets variable symbols.

**I**_{F}mapsto functions**D**→**D***(here**D**is a set of all sequences of any finite length over the domain**D***)**D**- This mapping interprets positional terms.

**I**_{SF}interprets terms with named arguments. It is a total mapping from`Const`to the set of total functions of the form`SetOfFiniteBags`(`ArgNames`×) →**D**. This is analogous to the interpretation of positional terms with two differences:**D**Each pair

`<s,v>`∈`ArgNames`×represents a argument/value pair instead of just a value in the case of a positional term.**D**- The arguments of a term with named arguments constitute a finite bag of argument/value pairs rather than a finite ordered sequence of simple elements.

Bags (multisets) are used here because the order of the argument/value pairs in a term with named arguments is immaterial and the pairs may repeat. For instance,

`p(a->b a->b)`.

**I**_{frame}is a total mapping fromto total functions of the form**D**`SetOfFiniteBags`(×**D**) →**D**.**D**This mapping interprets frame terms. An argument,

`d`∈, to**D****I**_{frame}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**I**_{frame}is used to determine the truth valuation of frame terms.Bags are used here because the order of the attribute/value pairs in a frame is immaterial and pairs may repeat. For instance,

`o[a->b a->b]`.

**I**_{sub}gives 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 a restriction in Section Interpretation of Formulas.

**I**_{isa}gives meaning to class membership. It is a total function×**D**→**D**.**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**_{=}gives meaning to the equality. It is a total function×**D**→**D**.**D****I**_{Truth}is a total mapping→**D**.**TV**- It is used to define truth valuation of formulas.

We also define the following mapping * I* :

(k) =**I****I**_{C}(k), if k is a symbol in`Const`(?v) =**I****I**_{V}(?v), if ?v is a variable in`Var`(f(t**I**_{1}... t_{n})) =**I**_{F}((f))(**I**(t**I**_{1}),...,(t**I**_{n}))(f(**I**`s`_{1}`->v`_{1}...`s`_{n}`->v`_{n})) =**I**_{SF}((f))({**I**`<s`_{1},(v**I**_{1})`>`,...,`<s`_{n},(v**I**_{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}),(v**I**_{1})`>`, ...,`<`(**I**`a`_{n}),(v**I**_{n})`>`})- Here {...} denotes a bag 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**_{=}((x),**I**(y))**I**

* The effect of data types.* The data types in

*impose the following restrictions. If*

**DTS**`dt`is a symbol space identifier of a data type, let

**LS**_{dt}denote the lexical space of

`dt`,

**VS**_{dt}denote its value space, and

**L**_{dt}:

**LS**_{dt}→

**VS**_{dt}the lexical-to-value-space mapping (for the definitions of these concepts, see Section Primitive Data Types of RIF-FLD). Then the following must hold:

**VS**_{dt}⊆; and**D**For each constant

`lit^^dt`∈**LS**_{dt},**I**_{C}(`lit^^dt`) =**L**_{dt}(`lit`).That is,

**I**_{C}must map the constants of a data type`dt`in accordance with**L**_{dt}.

RIF-BLD does not impose restrictions on **I**_{C} for constants in the lexical spaces that do not correspond to primitive datatypes in * DTS*.

### Interpretation of Formulas

* Truth valuation* 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 precisely the expected properties, it is required that

**I**_{Truth}((**I**`x = y`)) =**t**if and only if(**I**`x`) =(**I**`y`) and that**I**_{Truth}((**I**`x = y`)) =**f**otherwise.

*Subclass*:*TVal*_{I}(`sc ## cl`) =**I**_{Truth}((**I**`sc ## cl`)).To ensure that the operator

`##`is transitive, i.e.,`c1 ## c2`and`c2 ## c3`imply`c1 ## c3`, the following is required: For all`c1`,`c2`,`c3`∈,**D**`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`)).To ensure that all members of a subclass are also members of the superclass, i.e.,

`o # cl`and`cl ## scl`implies`o # scl`, the following is required: For all`o`,`cl`,`scl`∈,**D**`min`_{t}(*TVal*_{I}(`o # cl`),*TVal*_{I}(`cl ## scl`)) ≤_{t}*TVal*_{I}(`o # scl`).

*Frame*:*TVal*_{I}(`o[a`_{1}`->v`_{1}`... a`_{k}`->v`_{k}`]`) =**I**_{Truth}((**I**`o[a`_{1}`->v`_{1}`... a`_{k}`->v`_{k}`]`)).- Since the different attribute/value pairs are supposed to be understood as conjunctions, the following is required:
*TVal*_{I}(`o[a`_{1}`->v`_{1}`... a`_{k}`->v`_{k}`]`) =`min`_{t}(*TVal*_{I}(`o[a`_{1}`->v`_{1}`]`), ...,*TVal*_{I}(`o[a`_{k}`->v`_{k}`]`))

- Since the different attribute/value pairs are supposed to be understood as conjunctions, the following is required:
*Conjunction*:*TVal*_{I}(`And(`c_{1}... c_{n}`)`) =`min`_{t}(*TVal*_{I}(c_{1}), ...,*TVal*_{I}(c_{n})).*Disjunction*:*TVal*_{I}(`Or(`c_{1}... c_{n}`)`) =`max`_{t}(*TVal*_{I}(c_{1}), ...,*TVal*_{I}(c_{n})).*Quantification*:*TVal*_{I}(`Exists``?v`_{1}...`?v`_{n}(φ)) =`max`_{t}(*TVal*_{I*}(φ)) and*TVal*_{I}(`Forall``?v`_{1}...`?v`_{n}(φ)) =`min`_{t}(*TVal*_{I*}(φ)).Here

`max`_{t}(respectively,`min`_{t}) is taken over all interpretations* of the form <**I**,**TV**,**DTS**,**D****I**_{C},***I**_{V},**I**_{F},**I**_{frame},**I**_{SF},**I**_{sub},**I**_{isa},**I**_{Truth}>, which are exactly like, except that the mapping**I*****I**_{V}, is used instead of**I**_{V}.***I**_{V}is defined to coincide with**I**_{V}on all variables except, possibly, on`?v`_{1},...,`?v`_{n}.*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

*such that*

**I***TVal*

_{I}(φ) =

**t**for every φ∈Ψ. In this case, we write

**I**`|=`Ψ.

### 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 set 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

*of*

**I****R**and every ψ ∈

**R**, it is the case that

*TVal*

_{I}(ψ) ≤

*TVal*

_{I}(φ).

Equivalently, we can say that **R** `|=` φ holds iff whenever **I**`|=` **R** it follows that also **I**`|=` φ.