This document specifies the Core Logic Programming Dialect based on the well-founded semantics for default negation, RIF-CLPWD, a language for exchanging rules among systems that are based on the Logic Programming paradigm with the well-founded semantics. The RIF-CLPWD presentation syntax and semantics are specified as specializations of the RIF Framework for Logic Dialects (RIF-FLD). The XML serialization syntax of RIF-CLPWD is also given as a specialization of the XML syntax of RIF-FLD.
Table of Contents |
This specification develops RIF-CLPWD, the Core Logic Programming Dialect based on the well-founded semantics for default negation. RIF-CLPWD is intended to capture the paradigm of declarative logic programming that is based on the well-founded semantics (WFS) [GRS91,Prz94]. RIF-CLPWD is defined here as a specialization of the RIF framework for logic-based dialect [RIF-FLD], and high level of familiarity with RIF-FLD as well as with the well-founded semantics for default negation is assumed.
Syntactically, RIF-CLPWD corresponds to the language of rules with function symbols and negation (both default and explicit), where rule heads cannot contain disjunctions or equality. From the expressive power point of view, knowledge representation based on such rules is incomparable to the other popular logic programming paradigm, one that is based on answer-set programming (ASP) [GLe02]. One of the frequently cited difference is that ASP supports reasoning by cases, which is not possible using WFS. On the other hand, RIF-CLPWD is Turing-complete. Also, ASP is based on two-valued models, while WFS uses three-valued models. Due to the differences in their expressive power, the two paradigms are typically used for different purposes. WFS-based systems are normally used as programming languages in their own right. In contrast, ASP systems usually appear as embedded knowledge base components of imperative programming languages and are best suited for solving hard combinatorial problems.
Compared to standard logic programming, RIF-CLPWD has a number of syntactic extensions that are supported by most RIF dialects. These include objects and frames as in F-logic [KLW95], internationalized resource identifiers (or IRIs, defined by [RFC-3987]) as identifiers for concepts, and XML Schema datatypes [XML-SCHEMA2].
Compared to RIF-BLD [RIF-BLD], RIF-CLPWD does not support equality in rule conclusions, which reflects the limitations of most WFS-based systems (such support should be provided by dialects that are more expressive than this core logic programming dialect). On the other hand, it supports two kinds of negation, Naf (default negation with the WFS semantics) and Neg (the explicit negation). Thus, RIF-CLPWD is a proper extension of [RIF-Core], but, due to the exclusion of equality in rule heads, it is incomparable in its expressive power to RIF-BLD.
The following examples illustrate the key syntactic features of RIF-CLPWD, which are not found in RIF-BLD.
Unlike RIF-BLD, the well-founded semantics is three-valued. This example is a simple illustration of this property.
Document( Prefix(br <http://example.com/haircut#>) Prefix(hu <http://example.com/humanity#>) Group ( Forall ?P ( br:shaves(br:barber ?P) :- And (hu:person(?P) Naf br:shaves(?P ?P)) ) hu:person(br:barber) hu:person(hu:JoePublic) ) )In this example, the ground atomic formula hu:person(br:barber) is assigned the truth value u (undefined), while hu:person(hu:JoePublic) has the truth value t (true). Other facts, such as hu:person(hu:Mary), are false (f). ☐
The following example illustrates the use of both explicit and default negation.
The first rule here says that an individual would not be afraid of Math, if he is a student and it is not known (not explicitly stated) that that individual is not afraid of Math. Not being explicitly stated is expressed here by means of explicit negation Neg, while not being known is expressed by means of the default negation Naf. The second rule says that if an individual is a student majoring in Math then it is explicitly stated that that individual is unafraid of Math.
Document( Prefix(ex <http://example.com/concepts#>) Group ( Forall ?S ( ex:afraid(?S ex:Math) :- And ( ?S#ex:Student (Naf Neg ex:afraid(?S ex:Math)) ) ) Forall ?S ( Neg ex:afraid(?S ex:Math) :- And ( ?S#ex:Student ?S[ex:majors -> ex:Math] ) ) ) )
If we also had the facts ex:Joe#ex:Student and ex:Joe[ex:majors -> ex:Math] then we could conclude Neg ex:afraid(ex:Joe ex:Math) by the second rule. We will also be able to infer ex:afraid(ex:Joe ex:Math) by the first rule, which intuitively is a contradiction. In the RIF-CLPWD semantics, the well-founded model of such a knowledge base is said to be inconsistent. However, this does not destroy the KB completely in the sense that not everything is derivable. For instance, ex:afraid(ex:Nancy ex:Math) is derivable, but Neg ex:afraid(ex:Nancy ex:Math) is not. In a correctly built knowledge base, the above rules would have to be adjusted to avoid unintended conclusions (for example, by adding a conjunct of the form Naf ?S[ex:majors -> ex:Math] to the body of the first rule). ☐
The presentation syntax of the RIF Core Logic Programming Dialect with the well-founded semantics is defined by specialization from the presentation syntax of the RIF Syntactic Framework for Logic Dialects described in [RIF-FLD]. Section Syntax of a RIF Dialect as a Specialization of the RIF Framework in [RIF-FLD] lists the parameters of the syntactic framework in mathematical English, which we will now specialize for RIF-CLPWD.
All extension points of RIF-FLD are removed (specialized by replacing them with zero objects).
The alphabet of the RIF-CLPWD presentation syntax is identical to the alphabet of RIF-FLD.
Unlike RIF-BLD, RIF-CLPWD does not impose strict separation between individuals, predicates, and functions. As a result, the signature structure is much simplified. More specifically, RIF-CLPWD contains the following signatures:
The signature individual{ } represents the context in which individual objects can appear. The signature atomic is the standard signature of RIF-FLD, which represents the context where atomic formulas can occur.
In the definitions of the remaining signatures, below, the symbol Τ stands for either individual or atomic.
The above arrow expressions imply that an equality term is both an atomic formula and an individual. Therefore, such terms can occur anywhere an individual can occur, including arguments to predicates, functions, and so on.
Note that this allows frame terms to occur as arguments to predicates, functions, or as components in frame terms.
Again, this allows membership terms to occur as arguments to predicates, functions, or other terms.
As with frames and membership terms, this allows subclass terms to occur inside other terms.
Thus, a symbol can can appear in the position of an individual, a function, or a predicate without restrictions. However, the same symbol cannot represent both an external function/predicate and a regular one. This follows from the additional restrictions below.
RIF-CLPWD uses no special syntax for declaring signatures. Instead, the rule author specifies signatures contextually. That is, since RIF-CLPWD requires that each symbol can be either an external symbol or a regular symbol, if the same symbol occurs as both in different contexts then the parser must treat this as a syntax error. If no errors are found, all terms and atomic formulas are guaranteed to be well-formed. Thus, signatures are not part of the RIF-CLPWD language, and individual, atomic, list, fp, etc., are not reserved keywords.
It thus follows that a predicate or a function symbol, s, that occurs in an external term External(s(...)) cannot also occur as a non-external symbol.
RIF-CLPWD requires the symbol spaces defined in Section Constants, Symbol Spaces, and Datatypes of [RIF-DTB].
RIF-CLPWD supports the following types of formulas (see Well-formed Terms and Formulas in [RIF-FLD] for the definitions):
A RIF-CLPWD condition is an atomic formula, an external atomic formula, a negated (normal or external) atomic formula, or it is composed of such formulas using conjunctions and disjunctions. All these can be optionally preceded with existential quantifiers. A negated atomic formula has the form or either Neg φ, Naf ψ, or Naf Neg φ, where φ is a normal atomic formula and ψ is a normal or external atomic formula, i.e., classical negation cannot be applied to external atomic formulas.
A RIF-CLPWD rule is a RIF-FLD rule implication or a universally quantified RIF-FLD rule with the following restrictions:
A RIF-CLPWD rule can have free (non-quantified) variables. The semantics of RIF-CLPWD treats them as if they were implicitly quantified outside of the rule (i.e., if r is a rule with a free variable ?X then this is considered to be equivalent to Forall ?X (r)).
A RIF-CLPWD fact is a (optionally universally quantified) atomic formula or a negated atomic formula that does not include Naf. Free variables in such facts are assumed to be implicitly universally quantified.
A RIF-CLPWD group is a RIF-FLD group formula that contains only RIF-CLPWD rules, RIF-CLPWD facts, and RIF-CLPWD groups.
A RIF-CLPWD document is a RIF-FLD document that consists of directives and a RIF-CLPWD group formula. There is no Module directive. The Dialect directive must be Dialect("RIF-CLPWD"), and the Import(<loc>) directive (with one argument) can import RIF-CLPWD documents only. Here loc must be a Unicode character sequence that forms an IRI. There are no CLPWD-specific restrictions on the two-argument directive Import except that the second argument must be a Unicode sequence of characters of the form <loc>, where loc is an IRI.
The semantics of the RIF Core Logic Programming Dialect Dialect is defined by specialization from the semantics of the RIF framework for logic dialects. Section Semantics of a RIF Dialect as a Specialization of the RIF Framework in [RIF-FLD] lists the parameters of the semantic framework that can be specialized. Thus, for RIF-CLPWD, we need to look at the following parameters:
The restrictions on the signatures of symbols, terms, or formulas in RIF-CLPWD do not affect the semantic definitions of RIF-FLD in any significant way.
The set TV of truth values in RIF-CLPWD consists of three values, t, f, and u (undefined), such that f <_{t} u <_{t} t.
The set of data types and DTS of RIF-CLPWD includes the datatypes listed in Section Datatypes of [RIF-DTB].
The semantics of the two-argument Import directive is given in [RIF-RDF+OWL]. The semantics of the one-argument directive is the same as in RIF-FLD.
Truth valuation of a rule of the form head :- body is defined as follows. This definition is a specialization of the corresponding definition in RIF-FLD for the :- connective.
TVal_{I}(head :- body) = t if and only if TVal_{I}(head) ≥_{t} TVal_{I}(body). Otherwise, TVal_{I}(head :- body) = f.
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-CLPWD, this set is defined in Section Intended Models.
The well-founded semantics [GRS91,Prz94] is typically defined with respect to Herbrand domains [CL73], so we limit our attention to RIF-FLD semantic structures I = <TV, DTS, D, I_{C}, I_{V}, I_{F}, I_{NF}, I_{list}, I_{tail}, I_{frame}, I_{sub}, I_{isa}, I_{=}, I_{external}, I_{connective}, I_{truth}> that all have the same RIF-CLPWD-Herbrand domain. We say RIF-CLPWD-Herbrand domain and not simply a Herbrand domain because RIF-CLPWD has many more kinds of terms than the standard classical logic. This even includes certain formulas, such as membership, subclass, and frames. The semantics of RIF-FLD, which we are specializing here, is defined in a general way in which all such terms are mapped into the domain. Therefore, we need to define RIF-CLPWD-Herbrand domains, a generalization of the classical notion of Herbrand domains.
In what follows, we will be relying on the notions of ground terms, Herbrand Universe and Herbrand Domain, Herbrand Semantic Structure, minimal models, and other notions defined in Appendix: A Subframework for Herbrand Semantic Structures of the RIF FLD specification.
Definition (Intended Models - General).
Let Γ be a RIF-CLPWD document and Γ^{*}
be its ground instantiation. We say a RIF Herbrand semantic
multi-structure Î
of Γ is its intended model if and only
if Î is an intended model of Γ^{*}.
The remainder of this section defines the notion of intended
models of ground RIF-CLPWD documents.
☐
To define intended models for ground documents, we need to introduce the following notion of a program quotient (sometimes also called Gelfond-Lifshitz reduct). For the purpose of the next definition, we introduce three additional propositions that correspond to the three truth values of RIF-CLPWD: true, false, and undefined, such that for any RIF Herbrand semantic structure, I, TVal_{I}(true) = t, TVal_{I}(false) = f, and TVal_{I}(undefined) = u. (Note that for true we could have used And() and for false Or(). But no substitute exists in RIF-FLD for undefined.)
Definition (Quotient). Let Γ be a ground RIF-CLPWD document and Î a RIF Herbrand semantic multi-structure for it. The quotient of Γ with respect to Î, denoted Γ/ Î is a RIF-CLPWD document obtained as follows:
The resulting document is called the quotient of Γ with respect to Î and is denoted Γ/ Î.
It is easy to see that Γ/ Î does not contain atomic formulas that are negated with Naf. ☐
Observe that any quotient Γ/ Î is a Horn-like rule set in that it does not use default negation. We say Horn-like because these rules can still have explicit negation Neg. However, explicit negation behaves monotonically and this means that such rules have a unique minimal model. This model is computed by an iterative process of making all possible inferences using the rules in Γ/ Î starting with the empty RIF Herbrand semantic structure in which I_{true} maps everything to u [vEK76].
Let Γ be a ground RIF-CLPWD document and Î a RIF Herbrand semantic multi-structure. The unique minimal model of Γ/ Î will be denoted by M_{min}(Γ/ Î).
The following definition is an adaptation from [Prz94].
Definition (Well-founded Models).
The well-founded model of a ground RIF-CLPWD document, Γ, is defined as a limit of the following transfinite sequence of RIF Herbrand semantic structures I^{0}, I^{1}, ....
The initial structure, I^{0} is the
empty structure defined in Appendix: A Subframework for Herbrand Semantic Structures of the RIF FLD specification.
Suppose that I^{m} has already been defined for every m<k, where k is some ordinal number. Then:
The limit of such a sequence is known to exist [Prz94] and is unique; it is reached for some, possibly transfinite, ordinal α, such that I^{α} = I^{α+1}. ☐
Note that although the above limit exists and therefore a well-founded model is unique, it might not be consistent. Here is a simple example that illustrates that:
Group ( ex:p Neg ex:p :- Naf ex:q )
It is easy to see that the well-founded model here makes both ex:p and Neg ex;p true and therefore is inconsistent. Example 2 is another illustration of such possible inconsistency. We are now ready to define intended models for ground RIF-CLPWD documents.
Definition (Intended Models - Ground). Let Γ be a ground RIF-CLPWD document. A RIF Herbrand semantic multi-structure Î of Γ is said to be an intended model of Γ if it is a consistent Herbrand semantic multi-structure and a well-founded model for Γ/ Î. ☐
As explained just before the above definition, the intended model does not always exist, due to the consistency requirement,
Example 3 (Intended and unintended models)
Going back to Example 1, the intended model here is the one that assigns hu:person(br:barber) the truth value u and hu:person(hu:JoePublic) the truth value t. Other facts, such as hu:person(hu:Mary), are assigned the truth value f.
An example of an un-intended model would be one where hu:person(hu:Mary) is assigned t or u, as such conclusions are deemed to be unsupported. ☐
Section Mapping from the RIF-FLD Presentation Syntax to the XML Syntax of [RIF-FLD] defines a mapping, χ_{fld}, from the presentation syntax of RIF-FLD to its XML serialization. When restricted to well-formed RIF-CLPWD formulas, χ_{fld} becomes the CLPWD-to-XML mapping χ_{clpwd}. In this way, the XML serialization of RIF-CLPWD is a specialization of the RIF-FLD XML Serialization Framework defined in [RIF-FLD].
If T is a set of datatypes and symbol spaces and E a coherent set of external schemas for functions and predicates, then the general definition of conformance in RIF-FLD yields the notion of conformant CLPWD_{T,E} producers and consumers.
TBD