Notes on Semantic Structures
Rationale: There are several equivalent ways to define first-order semantic structures. The one we adopted has the advantage that it generalizes to rule sets with negation as failure (NAF) and to logics for dealing with uncertainty and inconsistency. The difficulty is that some popular theories for NAF, such as the well-founded semantics, are based on three-valued semantic structures. Some popular ways to handle uncertain or inconsistent information (which is certainly important in the Web environment) rely on four-valued and other multi-valued logics. Therefore, following M. Fitting, Fixpoint Semantics for Logic Programming A Survey, Theoretical Computer Science, 1999, we build our definitions to be compatible with future RIF dialects, which will be based multivalued logics.
Truth values: Some RIF dialects will have additional truth values. For instance, some versions of NAF use three truth values: t, f, and u (undefined). Handling of contradictions and uncertainty requires at least four truth values: t, u, f, and i (inconsistent).
Ordering truth values: In the well-founded semantics for NAF, f <t u <t t, and it is again a total order. But in four-valued logics, which are often used for dealing with uncertain or inconsistent information, the truth order is partial: f <t u <t t and f <t i <t t. Such logics also have another partial order, called the knowledge order <k: u <k t <k i; and u <k f <k i. Under the knowledge order, true and false are incomparable, and facts that are both true and false receive the truth value i, which is the least upper bound of f and t in the knowledge order.
Using sorts to simulate FOL, RDF, and other logics: Recall that RIF Core uses the symbols from Const to denote constants, predicates, and function symbols alike, so the same symbol can occur in multiple contexts. However, sometimes it is useful to restrict the contexts in which various symbols are allowed to occur. For instance, Prolog or RDF don't place any such restrictions, but OWL-DL has a unique role for each symbol. This restriction of the context is accomplished by controlling the sorts that are associated with each constant. For instance, if we do not want integers to occur as predicate and function symbols then we will not associate any arrow or Boolean sorts with the constants that are associated with the primitive sort integer. On the other hand, we do want URIs to denote concepts and other predicates. In that case, we would associate every Boolean sort with every constant that has a primitive sort URI. If we want to also allow local names for concepts and other predicates, then we might introduce a separate primitive sort, local, and allow the symbols that belong to this sort to have Boolean types.
RIF multisorted logic can also easily represent the syntax of the usual first order predicate calculus. To this end, we just need to ensure that each symbol in Const has exactly one sort associated with it. It could be a primitive sort, an arrow sort, or a Boolean sort, but it must be exactly one. In this case, any given symbol can occur either as a constant, or as a function symbol of one particular arity, or as a predicate of one particular arity.
Polymorphic constants: Association of multiple sorts with the same constant can be achieved with the help of equality. For instance, an assertion "foo"^^sort1 = "foo"^^sort2 ensures that these two constants represent the same entity, which therefore must belong simultaneously to sorts sort1 and sort2. If we want short integers to be also treated as a subsort of long integers, we can assert an equality "xyz"^^short = "xyz"^^long for every short integer xyz (in the range 0 through 216).
Intended models for rule sets: The notion of a model is only the basic ingredient in the definition of a semantics of a rule set. In general, a semantics of a rule set R is the set of its intended models (see Y. Shoham. Nonmonotonic logics: meaning and utility. In: Proc. 10th International Joint Conference on Artificial Intelligence, Morgan Kaufmann, pp. 388--393, 1987). There are different theories of what the intended sets of models are supposed to look like depending on the features of the particular rule sets.
For Horn rules, which we use in this section, the intended set of models of R is commonly agreed upon: it is the set of all models of R.
However, when rule bodies contain literals negated with the negation-as-failure connective naf, then only some of the models of a rule set are viewed as intended. This issue will be addressed in the appropriate dialects of RIF. The two most common theories of intended models are based on the so called well-founded models and stable models. Here we will just illustrate the problem with a simple example.
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: one in which p is true and one 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 will derive p even though it does not logically follow from p \/ q. The logic underlying rule-based systems also assumes that only the minimal models as intended (minimality here is with respect to the set of true facts). Therefore, the intended models of the above rule set R must have the property that not only p is true but also that q is false.