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

Notes about the Rationale for the Changes

This document is a version of "A.1_Basis:_Positive_Conditions". It proposes a modified syntax and semantics to account for Web-izing (the use of URIs for constants, predicates, and functions) and primitive data types (integers, floats, time, date, etc.). The main change is that there is no longer a wall between the domains of constants, functions, and predicates. Instead, all these symbols are now drawn from the same domain. Separation between the different kinds of symbols is introduced through the mechanism of sorts. For instance, we can introduce a sort URI for URIs and the sorts integer, float, time, string, etc. We can decide that certain sorts must be disjoint (integers, time) and others are not (eg, URI can be a subsort of string). We can control what sorts can be used for predicates, function symbols, etc. For example, we can decide that only strings can be predicates (which includes URIs, if URI is a subsort of string). Or we can decide that only URI and localSymbol (where localSymbol is some kind of a subsort of string) can be predicates and functions.

The first few sections on the syntax and semantics simply rework the material from "A.1_Basis:_Positive_Conditions" using the single domain for constants, functions, and predicates. The multisorted extension is described in sections Multisorted Extensions of the RIF Core, Formalization of Multisorted Syntax, and Semantics of the Multisorted RIF Core.

Introduction

The basis of the language is formed by what can appear in the bodies of Horn-like rules with equality -- conjunctions and disjunctions of atomic formulas and equations (such rules reduce to pure Horn). We later extend our proposal to include builtins. As mentioned in the introduction, the motivation is that this sublanguage can be shared among the bodies of the rules expressed in the following RIF dialects:

This sublanguage can also be used to uniformly express:

SYNTAX

Essential BNF for human-readable syntax:

  Var        ::= '?' NAME
  TERM       ::= Var | Expr
  Expr       ::= Con '(' TERM* ')' | Con
  Atom       ::= Expr | TERM '=' TERM
  LITFORM    ::= Atom
  QUANTIF    ::= 'Exists' Var+ '(' CONDIT ')'
  CONJ       ::= 'And' '(' CONDIT* ')'
  DISJ       ::= 'Or' '(' CONDIT* ')'
  CONDIT     ::= LITFORM | QUANTIF | CONJ | DISJ

Here LITFORM stands for Literal Formula and anticipates the introduction of negated atoms later on. QUANTIF stands for Quantified Formula, which |for Horn-like conditions can only be 'Exists' Formulas (Var+ variables should occur free in the scoped CONDIT, so 'Exists' can quantify them; free variables are discussed below). More explicitly than in logic programming, CONJ expresses formula conjunctions, and DISJ expresses disjunctions. Finally, CONDIT combines everything and defines RIF conditions, which can later be extended beyond LITFORM, QUANTIF, CONJ, or DISJ.

We assume that all constants (Con) belong to one logical sort: the sort of elementary entities. Relation names and function symbols are also in Con. This will be subsequently refined to allow multiple sorts for different data types. See "Sorted Extensions of the RIF Core".

At this point we do not commit to any particular vocabulary for the names of variables and for constants. For instance, NAME could be any alphanumeric string and a variety of options could be used for Con. We leave the decision till later time.

In the present version, variables are not sorted and thus can range over all constants. Sorted variables might be introduced in a later version of the language.

Note that there are two uses of variables in the RIF Condition Language: free and quantified. All quantified variables are quantified explicitly, existentially (and also universally, later). We adopt the usual scoping rules for quantification from first-order logic. Variables that are not explicitly quantified are free.

The free variables are needed because we are dealing with conditions that occur in rule bodies only. When a condition occurs in such a rule body, the free variables in the condition are precisely those that also occur in the rule head. Such variables are quantified universally outside of the rule, and the scope of such quantification is the entire rule. For instance, the variable ?X in the rule below is free in the condition that occurs in the rule body, but it is universally quantified outside of the rule.

Condition with a free variable ?X:
                             ... Exists ?Y (condition(..?X..?Y..)) ...

Rule using the condition in its body:
Forall ?X (head(...?X...) :- ... Exists ?Y (condition(..?X..?Y..)) ...)

When conditions are used as queries, their free variables are to be bound to carry the answer bindings back to the caller.

The semantics of conditions is defined in the section SEMANTICS.

Example 1 (A RIF condition in human-readable syntax):

  In this condition, ?Buyer is quantified existentially, while ?Seller
  and ?Author are free:

  And ( Exists ?Buyer (purchase(?Buyer ?Seller book(?Author LeRif) $49))
        ?Seller=?Author )

This syntax is similar in style, and compatible to, the OWL Abstract Syntax http://www.w3.org/TR/owl-semantics/syntax.html.

An XML syntax can be obtained from the above BNF as follows. The non-terminals in all-upercase such as CONDIT become XML entities, which act like macros and will not be visible in instance markups. The other non-terminals and symbols ('=', 'Exists', etc.) become XML elements, which are adapted from RuleML as shown below.

- Con (constant)
- Var (logic variable) 
- Expr   (expression formula)
- Atom   (atomic formula)
- Equal  (prefix version of term equation '=')
- Exists (quantified formula for 'Exists')
- And    (conjunction)
- Or     (disjunction)

Based on the FOL RuleML http://www.w3.org/Submission/FOL-RuleML experience, this could be directly rewritten as a DTD or an XML Schema.

The condition formula in Example 1 can be serialized in XML as shown below.

Example 2 (A RIF condition in XML syntax):

  <And>
    <Exists>
      <Var>Buyer</Var>
      <Atom>
        <Con>purchase</Con>
        <Var>Buyer</Var>
        <Var>Seller</Var>
        <Expr>
          <Con>book</Con>
          <Var>Author</Var>
          <Con>LeRif</Con>
        </Expr>
        <Con>$49</Con>
      </Atom>
    </Exists>
    <Equal>
      <Var>Seller</Var>
      <Var>Author</Var>
    </Equal>
  </And>

SEMANTIC STRUCTURES (a.k.a. INTERPRETATIONS)

The first step in defining a model-theoretic semantics for a logic-based language is to define the notion of a semantic structure, also known as interpretation, and then to define the notion of truth valuation for the formulas in the language.

In case of the first-order semantics, the setting given here is one of the standard common definitions. Although it is not as frequently used as some other well-known definitions of semantic structures, it has the advantage of being easy to generalize to non-first-order cases --- for instance, rule sets with negation as failure (NAF), some of which (e.g., well-founded negation) use three-valued semantic structures, and settings, such as the Web, where information can be uncertain or contradictory. In the latter case, four-valued and other multi-valued semantic structures are used. (See, for example, M. Fitting, Fixpoint Semantics for Logic Programming A Survey, Theoretical Computer Science, 1999.)

A semantic structure is a mappings of the form

I: Set of formulas → TV

where TV is the set of all truth values. Thus, if φ if a formula then I(φ) is its truth value.

The set of truth values TV typically has only two values, t and f. However, some versions of NAF have three, t, u (undefined), and f, and, as we remarked, treatment of contradictions and uncertainty requires at least four: t, u, f, and i (inconsistent).

The set TV is assumed to have a total or partial order, called the truth order; it is denoted <t. For instance, in the first-order case, f <t t, and it is a total order. In the well-founded semantics, f <t u <t t, and it is again a total order. But in Belnap-style four-valued logics, which are suitable for dealing with uncertain or inconsistent information, the truth order is partial: f <t u <t t and f <t i <t t.

As a side remark, Belnap-style logics also have another 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.

More formally, let us define the following sets:

An interpretation I consists of four mappings:

Using these mappings, we can define a more general mapping, I, as follows:

As explained earlier, an interpretation is supposed to map formulas to truth values. We define this mapping now:

Multisorted Extensions of the RIF Core

The classical idea of sorted logic can easily account for the ideas of primitive data types, URIs as identifiers of objects and concepts, and more. Many logic languages (e.g., Prolog, HiLog, F-logic, RDF) allow the same symbol to play multiple roles. For instance, the same symbol foo can be used as a constant, a predicate of several different arities, and as a function symbol of different arities. To account for such languages, we will use a multisorted logic.

In a multisorted RIF core, each constant from Con is associated with one or more sorts. A sort can be primitive, an arrow sort, or a Boolean sort. Arrow sorts are also known as function sorts and Boolean sorts are also known as predicate sorts.

Primitive sorts are drawn from a fixed collection of sorts PS1, ..., PSn. These sorts are intended to model primitive data types. For instance, we could have the sorts integer, strings, time, dates, etc. The same constant can be associated with more than one primitive sort, so it is possible that the sort of short integers will be a subsort of the sort of long integers (i.e., every constant that is associated with the sort short will also be associated with the sort long). It is a common practice to distinguish the constants of different primitive sorts syntactically. For instance, constants of the primitive sort integer, would have a different syntax from constants of sort string, and constants of primitive type URI would have yet another syntax.

An arrow sort is a statement of the form s1 × ... × sk → s, where s1, ..., sk, s are names of primitive sorts (i.e., one of the PS1, ..., PSn). A Boolean sort is a statement of the form s1 × ... × sk, where, again, s1, ..., sk are names of primitive sorts.

Recall that RIF core uses the symbols from Con to denote constants, predicates, and function symbols alike, so the same symbol can occur in multiple contexts. However, 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 one doesn't want integers to occur as predicate and function symbols then we don't associate any arrow or Boolean sorts with the constants that are associated with 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, localPred, and endow it with every Boolean type.

Formalization of Multisorted Syntax

Formally, the syntax of RIF core needs the following adjustments. We introduce new functions:

Each of these functions associates a (possibly empty) set of sorts (primitive, arrow, or Boolean) with every constant c ∈ Con.

PSort is also defined on variables:

The intended meaning is that if ?v ∈ Var and PSort(?v) = {s1, ..., sk} then ?v can be bound only to function terms that are simultaneously of sorts s1, ..., sk (we define what it means for a function term to belong to a primitive sort below). In theory, PSort(?v) can be an empty set. However, such a variable would be useless, since it cannot be bound to anything.

Well-formed function terms. If c ∈ Con is a constant and s ∈ PSort(c) then we say that c (and c(), which we identify with c) is a well-formed function term of sort s. Note that the same constant can be a well-formed term of several different sorts because we allow several primitive sorts to be associated with the same constant. The informal meaning of such a happenstance is that the term belongs to the "intersection" of all the sorts with which it is associated.

By induction, if f(t1, ..., tk) is a function term then it is a well-formed function term of sort s if there is an arrow sort s1, ..., sk → s ∈ ASort(f) such that t1, ..., tk are well-formed function terms of sorts s1, ..., sk, respectively.

It is convenient to extend the mapping PSort from constants to function terms as follows:

Well-formed atomic formula. We can now say that an atomic formula p(t1, ..., tk) is well-formed if and only if t1, ..., tk are well-formed function terms and there is a Boolean sort s1 × ... × sk ∈ BSort(p) such that s1PSort(t1), ..., sk ∈ PSort(tk).

The only other modification to the definition of the RIF syntax is that we must require that all atomic formulas that occur in RIF conditions and rules must be well-formed.

Semantics of the Multisorted RIF Core

The semantics of RIF core needs the following adjustments in order to be compatible with the multisorted syntax: