This is an archive of an inactive wiki and cannot be modified.

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.

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 truth order, such that f <t t.

Semantic Structures

A semantic structure, I, is a tuple of the form <TV, DTS, D, IC, IV, IF, Iframe, ISF, Isub, Iisa, I=, ITruth>. Here D is a non-empty set of elements called the domain of I, and there is a proper subset, Dind ⊂D, which is used to interpret individuals. We use Const to refer to the set of all constant symbols and Var to refer to 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:

We also define the following mapping I :

The effect of data types. The data types in DTS impose the following restrictions. If dt is a symbol space identifier of a data type, let LSdt denote the lexical space of dt, VSdt denote its value space, and Ldt: LSdtVSdt 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:

RIF-BLD does not impose restrictions on IC 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 TValI:

A model of a set Ψ of formulas is a semantic structure I such that TValI(φ) = 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 I of R and every ψ ∈ R, it is the case that TValI(ψ) ≤ TValI(φ).

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