• BLD
• Semantics

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 TV of truth values in RIF-BLD consists of just two values, t and f such that f <_t t. Clearly, <_t is a total order here.

• Data types.

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

    • xsd:long

    • xsd:integer

    • xsd:decimal

    • xsd:string

    • xsd:time

    • xsd:dateTime

    • rdf:XMLLiteral

    • rif:text

• Logical entailment.

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

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

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, I_C, I_V, I_F, I_frame, I_SF, I_sub, I_isa, I₌, I_Truth>. Here D is a non-empty set of elements called the domain of I, and there is a proper subset, D_ind ⊂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:

• 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.

• I_V maps Var to elements of D_ind.

  • This mapping interprets variable symbols.

• I_F maps D to functions D* → D (here D* is a set of all sequences of any finite length over the domain 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) → D. This is analogous to the interpretation of positional terms with two differences:

  • Each pair <s,v> ∈ ArgNames × D represents a 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 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 from D to total functions of the form SetOfFiniteBags(D × D) → D.

  • This mapping interprets frame terms. An argument, d ∈ D, to 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 :

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

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

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

• I(f(s₁->v₁ ... s_n->v_n)) = I_SF(I(f))({<s₁,I(v₁)>,...,<s_n,I(v_n)>})

  • Here we use {...} to denote a bag of argument/value pairs.

• I(o[a₁->v₁ ... a_k->v_k]) = I_frame(I(o))({<I(a₁),I(v₁)>, ..., <I(a_n),I(v_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₌(I(x), I(y))

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 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 ⊆ D; and

• 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₁ ... t_n)) = I_Truth(I(r(t₁ ... t_n)))

• Atomic formulas with named arguments: TVal_I(p(s₁->v₁ ... s_k->v_k)) = I_Truth(I(p(s₁-> v₁ ... 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₁->v₁ ... a_k->v_k]) = I_Truth(I(o[a₁->v₁ ... 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₁->v₁ ... a_k->v_k]) = min_t(TVal_I(o[a₁->v₁]), ..., TVal_I(o[a_k->v_k]))

• Conjunction: TVal_I(And(c₁ ... c_n)) = min_t(TVal_I(c₁), ..., TVal_I(c_n)).

• Disjunction: TVal_I(Or(c₁ ... c_n)) = max_t(TVal_I(c₁), ..., TVal_I(c_n)).

• Quantification: TVal_I(Exists ?v₁ ... ?v_n (φ)) = max_t(TVal_I*(φ))   and   TVal_I(Forall ?v₁ ... ?v_n (φ)) = 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_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₁,...,?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 I such that 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 I of 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 |= φ.