The RIF Framework for Logic-based Dialects (RIF-FLD) is a formalism for specifying all logic-based dialects of RIF, including RIF-BLD. It is a logic in which both syntax and semantics are described through a number of mechanisms that are commonly used for various logic languages, but are rarely brought all together. RIF-BLD gives precise definitions to these mechanisms, but leaves some concrete details out. Each dialect that is based on RIF-FLD is expected to specialize these general mechanisms (even leave out some elements of RIF-FLD) to produce its concrete syntax and model-theoretic semantics.
This document is intended for the designers of future RIF dialects. The reader who is interested in using a particular dialect, such as RIF-BLD, or in implementing such a dialect can go directly to the description of the dialect in question.
RIF-FLD has the following main components:
Syntactic framework. This framework defines the mechanisms for specifying the formal presentation syntax of RIF's logic dialects. The presentation syntax is used in RIF to define the semantics of the dialects and to illustrate the main ideas with examples. The presentation syntax of a dialect is not intended to be a concrete syntax for that dialect. For instance, RIF deliberately leaves out details such as the delimiters of the various syntactic components, escape symbols, parenthesizing, precedence of operators, and the like. Instead, being an interchange format, RIF dialects use XML as their concrete syntax.
Semantic framework. The semantic framework describes the mechanisms that are used for specifying the models of RIF logic-based dialects.
XML serialization framework. This framework defines the general principles that logic-based dialects are to use in specifying their concrete XML-based syntaxes. For each dialect, its concrete XML syntax is a derivative of the dialect's presentation syntax. It can be seen as a serialization of that syntax.
The framework described in this document is very general, and it captures most of the popular logic-based languages found in Databases, Logic Programming, and on the Semantic Web. However, it is expected that the needs of some newly developed dialects may stimulate further evolution of RIF-FLD.
Syntactic framework. The syntactic framework defines three main classes of RIF terms:
Positional terms. These are the usual terms, which are most commonly used in first-order logic. RIF-FLD defines positional terms in a slightly more general way in order to enable dialects with higher-order syntax, such as HiLog [CKW93].
Terms with named arguments. These are like positional terms except that each argument of a term is named and the order between the arguments is immaterial. Terms with named arguments correspond to rows in relational tables, where column headings correspond to argument names.
Frames. A frame term represents an assertion about an object and its properties. These terms correspond to molecules of F-logic [KLW95]. There is certain syntactic similarity between terms with named arguments and frames, since object properties resemble to named arguments. However, the semantics of these terms are quite different.
RIF dialects can choose to support all or some of the aforesaid categories of terms. The syntactic framework also defines the following mechanisms for specializing these terms:
Symbol spaces.
Symbol spaces are used to separate the set of all non-logical symbols (symbols used as variables, individual constants, predicates, and functions) into distinct subsets. These subsets can then be given different semantics. A symbol space has one or more identifiers and a lexical space, which defines the "shape" of the symbols in that symbol space. For instance, some symbol spaces can be used to identify any object, and syntactically they look like IRIs (for instance, rif:IRI in RIF Basic Logic Dialect). Other symbol spaces may be used to describe the data types used in RIF (for example, xsd:integer).
Signatures.
Signatures determine which terms and formulas are well-formed. It is a generalization of the notion of a sort in classical first-order logic [Enderton01]. Each nonlogical symbol (and some logical symbols, like =) has an associated signature. A signature defines, in a precise way, the syntactic contexts in which the symbol is allowed to occur.
For instance, the signature associated with a symbol, p, might allow p to appear in a term of the form f(p), but disallow it to occur in a term like p(a,b). The signature for f, on the other hand, might allow that symbol to appear in f(p) and f(p,q), but disallow f(p,q,r) and f(f). In this way, it is possible to control which symbols are used for predicates and which for functions, where variables can occur, and so on.
Semantic framework. This framework defines the notion of a semantic structure or interpretation (both terms are used in the literature [Enderton01, Mendelson97], but here we will mostly use the first). Semantic structures are used to interpret RIF formulas and to define logical entailment. As with the syntax, this framework includes a number of mechanisms that RIF logic-based dialects can specialize to suit their needs. These mechanisms include:
Truth values. RIF-FLD is designed to accommodate the dialects that support reasoning with inconsistent and uncertain information. Most of the logics that were designed to deal with these situations are multi-valued. Consequently, RIF-FLD postulates that there is a set of truth values, TV, which includes the values t (true) and f (false) and possibly others. For example, RIF Basic Logic Dialect is two-valued, but other dialects can be three-valued, four-valued, and so on.
Data types. Some symbol spaces (which are part of the RIF syntactic framework) may have special semantics. For instance, symbols in the symbol space of strings (xsd:string) are always interpreted as sequences of unicode characters, and a ≠ b for any pair of distinct symbols. Symbol spaces that have special semantics are called data types.
Entailment. This notion is fundamental to logic-based dialects. Given a set of formulas (e.g., facts and rules) G, entailment determines which other formulas necessarily follow from G. Entailment is the main mechanism underlying query answering in databases, logic programming, and the various reasoning tasks in Description Logic.
Roughly speaking, a set of formulas, G, logically entails another formula, g, if for every semantic structure I in some set S, if I makes G true, then I also makes g true. Almost all known logics define entailment this way. The difference lies in which set S they use. For instance, logics that are based on the classical first-order predicate calculus, such as Description Logic, assume that S is the set of all semantic structures. In contrast, logic programming languages, which use default negation, assume that S contains only the so-called "minimal" Herbrand models of G and, furthermore, only the minimal models of a special kind. See [Shoham87] for a more detailed exposition of this subject.
XML serialization framework. This framework defines the general principles for serializing the various parts of the presentation syntax of RIF-FLD.