RIF Core Logic Programming Dialect Based on the Well-founded Semantics

Specification 13 August 2010

Editors:

Michael Kifer, Stony Brook University, USA

---

Abstract

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.

1 Overview

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.

Example 1 (Barber).

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)
      )
)
    

Example 2 (Math Phobia).

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] )
	  )
      )
)
    

2 The Presentation Syntax of RIF-CLPWD as a Specialization of RIF-FLD

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.

1. Extension points.

   All extension points of RIF-FLD are removed (specialized by replacing them with zero objects).

2. Alphabet.

   The alphabet of the RIF-CLPWD presentation syntax is identical to the alphabet of RIF-FLD.

3. Assignment of signatures to each constant and variable symbol.

   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:

   1. Basic
      • individual{ }
      • atomic{ }

      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.

   2. Signatures for lists
      • The signature list for closed lists. It has the following arrow expressions: () ⇒ individual, (individual) ⇒ individual, (individual individual) ⇒ individual, ...
      • The signature openlist for open lists (that have tails). It has the following arrow expressions: (individual individual) ⇒ individual, (individual individual individual) ⇒ individual, ...
   3. Signatures for functions, predicates, and external functions and predicates
      • A signature for function and predicate symbols: fp. This signature has the arrow expressions for positional functions and predicates: () ⇒ Τ, (individual) ⇒ Τ, (individual individual) ⇒ Τ, ..., plus the arrow expressions for predicates with named arguments: (s1->individual ... sk->individual) ⇒ Τ, for all k>0 and all s1, ..., sk ∈ ArgNames.
   4. The signature for equality is ={(individual individual) ⇒ Τ}.

      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.

   5. The frame signature, ->, is ->{(individual individual individual) ⇒ Τ}.

      Note that this allows frame terms to occur as arguments to predicates, functions, or as components in frame terms.

   6. The membership signature, #, is #{(individual individual) ⇒ Τ}.

      Again, this allows membership terms to occur as arguments to predicates, functions, or other terms.

   7. The signature for the subclass relationship is ##{(individual individual) ⇒ Τ}.

      As with frames and membership terms, this allows subclass terms to occur inside other terms.

   8. Assignment of signatures to symbols:
      • Non-datatype symbols in Const, including the rif:iri and rif:local symbols, have the signatures individual, atomic, and, possibly, fp.

        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.

      • Symbols that correspond to RIF datatypes (XML Schema datatypes, rdf:XMLLiteral, rdf:PlainLiteral, etc.) all have the signature individual in RIF-CLPWD.
      • All variables have the signature individual, so they can range only over individuals.

   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.

4. Supported types of terms.
   • RIF-CLPWD supports the following types of terms defined by the syntactic framework (see the Section Terms of [RIF-FLD]):
     1. constants
     2. variables
     3. positional
     4. with named arguments
     5. lists
     6. equality
     7. frame
     8. membership
     9. subclass
     10. external
     11. formula
   • Compared to RIF-FLD, terms (both positional and with named arguments) have a number of restrictions:
     • Variables:
       The signature for the variable symbols does not permit them to occur in the context of predicate symbol, function symbol, or formulas. In particular, in the RIF-CLPWD specialization of RIF-FLD, a variable is not an atomic formula.
     • Functions and predicates:
       Signatures permit only constant symbols to occur in the context of function or predicate symbols. Indeed, RIF-CLPWD signatures ensure that all variables have the signature individual{ } and all other terms, except for the constants from Const, can have either the signature individual{ } or atomic{ }. Therefore, if t is a (non-Const) term (e.g., s(a)) then t(...) is not a well-formed term (e.g., s(a)(b)).
     • External predicates and functions:
       A term, t, may appear as an external term or an external atomic formula (i.e., in the context External(t)) if and only if t is an instantiation of an externally defined schema from the coherent set of external schemas associated with the language.

       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.

     • Formula terms:
       Only the formula terms described below in Supported formulas are allowed.
5. No aggregate terms or remote term references are allowed.
6. Required symbol spaces.

   RIF-CLPWD requires the symbol spaces defined in Section Constants, Symbol Spaces, and Datatypes of [RIF-DTB].

7. Supported formulas.

   RIF-CLPWD supports the following types of formulas (see Well-formed Terms and Formulas in [RIF-FLD] for the definitions):

   • RIF-CLPWD condition

     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.

   • RIF-CLPWD rule

     A RIF-CLPWD rule is a RIF-FLD rule implication or a universally quantified RIF-FLD rule with the following restrictions:

     • The conclusion of a rule is an atomic formula, an explicitly negated atomic formula (Neg φ), or a conjunction of such formulas.
     • None of the atomic formulas mentioned in the rule conclusion is externally defined (i.e., cannot have the form External(...)).
     • The premise of the rule is a RIF-CLPWD condition.

       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)).

   • RIF-CLPWD fact

     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.

   • RIF-CLPWD group

     A RIF-CLPWD group is a RIF-FLD group formula that contains only RIF-CLPWD rules, RIF-CLPWD facts, and RIF-CLPWD groups.

   • RIF-CLPWD document

     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.

3 The Semantics of RIF-CLPWD as a Specialization of RIF-FLD

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 effect of the syntax.

  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.

• Truth values.

  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.

• Datatypes.

  The set of data types and DTS of RIF-CLPWD includes the datatypes listed in Section Datatypes of [RIF-DTB].

• Directives, connectives.
  • Import directive.

    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.

  • The rule implication connective :-.

    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.

• Logical entailment.

  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.

3.1 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:

• For every rule or fact in Γ, replace every negated atomic formula of the form Naf φ according to its truth value TVal_I(Naf φ): if TVal_I(Naf φ) = t then Naf φ is replaced with the proposition true; if TVal_I(Naf φ) = f then it is replaced with false; otherwise, it is replaced with undefined.

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⁰, I¹, ....
The initial structure, I⁰ 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:

• I^k = M_min(Γ/ I^k-1), if k is a non-limit ordinal.
• I^k = ∪_i<k Iⁱ, if k is a limit ordinal.

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.    ☐

4 The XML Serialization of RIF-CLPWD as a Specialization of RIF-FLD

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].

5 RIF-CLPWD Conformance as a Specialization of 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.

6 Acknowledgements

TBD

7 References

7.1 Normative References

[RFC-3987]

RFC 3987 - Internationalized Resource Identifiers (IRIs), M. Duerst and M. Suignard, IETF, January 2005. This document is http://www.ietf.org/rfc/rfc3987.txt.

[RIF-BLD]

RIF Basic Logic Dialect Harold Boley, Michael Kifer, eds. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CR-rif-bld-20091001/. Latest version available at http://www.w3.org/TR/rif-bld/.

[RIF-Core]

RIF Core Dialect Harold Boley, Gary Hallmark, Michael Kifer, Adrian Paschke, Axel Polleres, Dave Reynolds, eds. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CR-rif-core-20091001/. Latest version available at http://www.w3.org/TR/rif-core/.

[RIF-DTB]

RIF Datatypes and Built-Ins 1.0 Axel Polleres, Harold Boley, Michael Kifer, eds. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CR-rif-dtb-20091001/. Latest version available at http://www.w3.org/TR/rif-dtb/.

[RIF-FLD]

RIF Framework for Logic Dialects Harold Boley, Michael Kifer, eds. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CR-rif-fld-20091001/. Latest version available at http://www.w3.org/TR/rif-fld/.

[RIF-RDF+OWL]

RIF RDF and OWL Compatibility Jos de Bruijn, editor. W3C Candidate Recommendation, 1 October 2009, http://www.w3.org/TR/2009/CR-rif-rdf-owl-20091001/. Latest version available at http://www.w3.org/TR/rif-rdf-owl/.

[XML1.0]

Extensible Markup Language (XML) 1.0 (Fourth Edition), W3C Recommendation, World Wide Web Consortium, 16 August 2006, edited in place 29 September 2006. This version is http://www.w3.org/TR/2006/REC-xml-20060816/.

[XML Schema Datatypes]

W3C XML Schema Definition Language (XSD) 1.1 Part 2: Datatypes. David Peterson, Shudi Gao, Ashok Malhotra, C. M. Sperberg-McQueen, and Henry S. Thompson, eds. W3C Candidate Recommendation, 30 April 2009, http://www.w3.org/TR/2009/CR-xmlschema11-2-20090430/. Latest version available as http://www.w3.org/TR/xmlschema11-2/.

7.2 Informational References

[CL73]

Symbolic Logic and Mechanical Theorem Proving, C.L. Chang and R.C.T. Lee. Academic Press, 1973.

[CURIE]

CURIE Syntax 1.0: A syntax for expressing Compact URIs, Mark Birbeck, Shane McCarron. W3C Working Draft 2 April 2008. Available at http://www.w3.org/TR/curie/.

[Enderton01]

A Mathematical Introduction to Logic, Second Edition, H. B. Enderton. Academic Press, 2001.

[GLe02]

Logic programming and knowledge representation - The A-Prolog perspective, M. Gelfond and N. Leone. Artificial Intelligence 138(1-2), pages 3-38, 2002.

[GLi88]

The Stable Model Semantics for Logic Programming, M. Gelfond and V. Lifschitz. Logic Programming: Proceedings of the Fifth Conference and Symposium, pages 1070-1080, 1988.

[GRS91]

The Well-Founded Semantics for General Logic Programs, A. Van Gelder, K.A. Ross, J.S. Schlipf. Journal of ACM, 38:3, pages 620-650, 1991.

[IS98]

Negation as Failure in the Head, K. Inoue and C. Sakama. Journal of Logic Programming, 35, pages 39-78, 1998.

[KLW95]

Logical foundations of object-oriented and frame-based languages, M. Kifer, G. Lausen, J. Wu. Journal of ACM, July 1995, pp. 741--843.

[Mendelson97]

Introduction to Mathematical Logic, Fourth Edition, E. Mendelson. Chapman & Hall, 1997.

[RIF-UCR]

RIF Use Cases and Requirements Adrian Paschke, David Hirtle, Allen Ginsberg, Paula-Lavinia Patranjan, Frank McCabe, eds. W3C Working Draft, 18 December 2008, http://www.w3.org/TR/2008/WD-rif-ucr-20081218/. Latest version available at http://www.w3.org/TR/rif-ucr/.

[vEK76]

The semantics of predicate logic as a programming language, M. van Emden and R. Kowalski. Journal of the ACM 23 (1976), pp. 733-742.

[Prz94]

Well-founded and stationary models of logic programs, T.C. Przymusinski. Annals of Mathematics and Artificial Intelligence 12 (1994), pp. 141-187.