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

Semantics of a RIF Dialect as a Specialization of RIF-FLD

The RIF-FLD semantic framework defines the notions of semantic structures and of models of RIF formulas. The semantics of a dialect is derived from these notions by specializing the following parameters.

All of the above notions are defined in the remainder of this document.

Truth Values

Each RIF dialect is expected to define the set of truth values, denoted by TV. This set must have a partial order, called the truth order, denoted <t. As a special case, <t can be a total order in some dialects. We write at b if either a <t b or a and b are the same element of TV. In addition,

RIF dialects can have additional truth values. For instance, the semantics of some versions of NAF, such as the well-founded negation, requires three truth values: t, f, and u (undefined), where f <t u <t t. Handling of contradictions and uncertainty usually requires at least four truth values: t, u, f, and i (inconsistent). In this case, the truth order is partial: f <t u <t t and f <t i <t t.

Primitive Data Types

A primitive data type (or just a data type, for short) is a symbol space that has

Semantic structures are always defined with respect to a particular set of data types, denoted by DTS. In a concrete dialect, DTS always includes the data types supported by that dialect. All RIF dialects are expected to support the following primitive data types:

Their value spaces and the lexical-to-value-space mappings are defined as follows:

Although the lexical and the value spaces might sometimes look similar, one should not confuse them. Lexical spaces define the syntax of the constant symbols in the RIF language that belong to the various primitive data types. In contrast, value spaces define the meaning of those constants. The lexical and the value spaces are often not even isomorphic. For instance, 1.2^^xsd:decimal and 1.20^^xsd:decimal are two legal -- and distinct -- 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. Therefore, 1.2^^xsd:decimal = 1.20^^xsd:decimal is a RIF tautology. Likewise, RIF semantics for data types implies certain inequalities. For instance, abc^^xsd:stringabcd^^xsd:string is a tautology, since the lexical-to-value-space mapping of the xsd:string type maps these two constants into distinct elements in the value space of xsd:string.

Semantic Structures

The central step in specifying a model-theoretic semantics for a logic-based language is defining the notion of a semantic structure, also known as an interpretation. Semantic structures are used to assign truth values to RIF-FLD formulas.

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. We will continue to 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.

The other components of I are total mappings defined as follows:

We also define the following mapping I :

The effect of signatures. For every signature, sg, supported by the dialect, there is a subset DsgD, called the domain of the signature. Terms that have a given signature, sg, are supposed to be mapped by I to Dsg, and if a term has more than one signature it is supposed to be mapped into the intersection of the corresponding signature domains. To ensure this, the following is required:

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. Then the following must hold:

RIF-FLD does not impose special requirements to IC for constants in the lexical spaces that do not correspond to primitive datatypes in DTS. Dialects may have such requirements, however. An example of such a restriction could be a requirement that no constant in a particular symbol space (such as rif:local) can be mapped to VSdt of a data type dt.

Interpretation of Formulas

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

Note that rules and equality formulas are two-valued even if TV has more than two values.

A model of a set R of formulas is a semantic structure I such that TValI(φ) = t   for every   φ∈R.

Intended Models

The semantics of a set of formulas, R, is the set of its intended semantic structures. RIF-FLD does not specify what these intended structures are, leaving this to RIF dialects. There are different theories of how the intended sets of semantic structures are supposed to look like.

For the classical first-order logic, every semantic structure is intended. For RIF-BLD, which is based on Horn rules, intended semantic structures are defined only for rulesets: an intended semantic structure of a RIF-BLD ruleset R is the unique minimal Herbrand model of R. For the dialects in which rule bodies may contain literals negated with the negation-as-failure connective naf, only some of the minimal Herbrand models of a rule set are intended. Each dialect of RIF is supposed to define the notion of intended semantic structures precisely. The two most common theories of intended semantic structures are the so called well-founded models [GRS91] and stable models [GL88].

The following example illustrates the notion of intended semantic structures. Suppose R consists of a single rule p :- naf q. If naf were interpreted as classical negation, not, then this rule would be simply equivalent to p \/ q, and so it would have two kinds of models: those where p is true and those where q is true. In contrast to first-order logic, most rule-based systems do not consider p and q symmetrically. Instead, they view the rule p :- naf q as a statement that p must be true if it is not possible to establish the truth of q. Since it is, indeed, impossible to establish the truth of q, such theories would derive p even though it does not logically follow from p \/ q. The logic underlying rule-based systems also assumes that only the minimal Herbrand models are intended (minimality here is with respect to the set of true facts). Furthermore, although our example has two minimal Herbrand models -- one where p is true and q is false, and the other where p is false, but q is true, only the first model is considered to be intended.

The above concept of intended models and the corresponding notion of logical entailment with respect to the intended models, defined below, is due to [Shoham87].

Logical Entailment

We will now define what it means for a set of RIF formulas to entail a RIF formula. We assume that each ruleset has an associated set of intended semantic structures.

Let R be a set of RIF formulas and φ a closed RIF formula. We say that R entails φ, written as R |= φ, if and only if for every intended semantic structure I of R and every ψ ∈ R, it is the case that TValI(ψ) ≤ TValI(φ).

This general notion of entailment covers both first-order logic and non-monotonic logics that underlie many rule-based languages [Shoham87].