W3C RuleML

RIF Core Answer Set Programming Dialect

Specification 17 December 2009

Editors:
Stijn Heymans, Vienna University of Technology, Austria
Michael Kifer, State University of New York at Stony Brook, USA

Abstract

This document specifies the Core Answer Set Programming Dialect, RIF-CASPD, a language for exchanging rules among systems that are based on the Answer Set Programming paradigm. The RIF-CASPD presentation syntax and semantics are specified as specializations of the RIF Framework for Logic Dialects (RIF-FLD). The XML serialization syntax of RIF-CASPD is also given as a specialization of the XML syntax of RIF-FLD.

Table of Contents

1 Overview

This specification develops RIF-CASPD, the Core Answer Set Programming Dialect. RIF-CASPD is intended to capture the paradigm of declarative logic programming that is based on the answer set semantics [GLe02] (it is also known as the stable model semantics [GLi88] when applied to a subset of the language). The ASP paradigm is especially useful as a way of specifying and solving NP-complete problems. RIF-CASPD is defined 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 ASP paradigm is assumed.

Syntactically, RIF-CASPD corresponds to the language of rules, without function symbols, where rule heads can contain disjunctions or be empty but cannot contain equality. From the expressive power point of view, ASP-based knowledge representation is incomparable to the other frequently used logic programming paradigm, one that is based on the well-founded semantics (WFS) [GRS91]. One of the frequently cited difference is that ASP supports reasoning by cases, which is not possible using WFS. Due to the differences in their expressive power, the two paradigms are typically used for different purposes. ASP is ideally suited for solving hard combinatorial problems and such systems usually appear as embedded knowledge base components of imperative programming languages. In contrast, WFS-based systems typically are Turing-complete and can be used as programming languages in their own right.

Syntactically, RIF-CASPD has a number of extensions (relative to standard logic programming) that are typical of 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-CASPD does not support equality in rule conclusions or function symbols in keeping with the practice of ASP solvers. On the other hand, it supports two kinds of negation, Naf (default negation with ASP semantics) and Neg (the explicit negation). In addition, unlike in RIF-BLD, rule conclusions can be disjunctions of atomic formulas or they might be empty. The latter form of rules corresponds to integrity constraints. This makes RIF-CASPD a proper extension of [RIF-Core], but it is incomparable in its expressive power with RIF-BLD.

The following examples illustrate the key syntactic features of RIF-CASPD, which are not found in RIF-BLD.

Example 1 (Some of the rules describing the Sudoku game).

This example shows two of the possible rules for specifying the Sudoku game. The first rule says that there can be any one of the nine possible digits in any box. The second rule is a constraint that says that the same digit cannot be in two different boxes the same row. Note that the facts introduce a subset of the Sudoku board using su:coordinates and a partial filling of the board using su:position.

Document(
      Prefix(su <http://example.com/sudoku#>)

      Group (
	  su:coordinates(1 1)
	  su:coordinates(1 2)
	  su:coordinates(2 1)
	  su:coordinates(2 2)
	  su:position(1 1 1)
	  su:position(1 2 2)

          Forall ?X ?Y (
	      Or ( su:position(1 ?X ?Y) su:position(2 ?X ?Y) su:position(3 ?X ?Y)
	           su:position(4 ?X ?Y) su:position(5 ?X ?Y) su:position(6 ?X ?Y)
	           su:position(7 ?X ?Y) su:position(8 ?X ?Y) su:position(9 ?X ?Y)
	      )  :- su:coordinates(?X ?Y)
          )
      
          Forall ?X1 ?X2 ?Y ?N (
	      :- And ( su:coordinates(?X1 ?Y) su:coordinates(?X2 ?Y)
		       su:position(?N ?X1 ?Y) su:position(?N ?X2 ?Y) 
		       Naf ?X1 = ?X2 )
          )
      )
)
    

The following example illustrates the use of both explicit and default negation.

Example 2 (Math Phobia).

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

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

The presentation syntax of the RIF Core Answer Set Programming Dialect 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-CASPD.

  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-CASPD presentation syntax is identical to the alphabet of RIF-FLD.

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

    Unlike RIF-BLD, RIF-CASPD does not impose strict separation between individuals, predicates, and functions. As a result, the signature structure is much simplified. More specifically, RIF-CASPD 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.

    2. Signatures for predicates, and external functions and predicates
      • Signature for regular (non-external) predicate symbols p. This signature has the arrow expressions for positional predicates: () ⇒ atomic, (individual) ⇒ atomic, (individual individual) ⇒ atomic, ..., plus the arrow expressions for predicates with named arguments: (s1->individual ... sk->individual) ⇒ atomic, for all k>0 and all s1, ..., skArgNames.
      • Signature for external function and predicate symbols efp. This signature has the following arrow expressions, where each occurrence of Τ stands for either individual or atomic: () ⇒ Τ, (Τ) ⇒ Τ, (Τ Τ) ⇒ Τ, ..., plus (s1->Τ ... sk->Τ) ⇒ Τ, for all k>0 and all s1, ..., skArgNames.

      Note: We may remove terms with named arguments, since they introduce implicit equalities like p(a→b c→d) = p(c→d a→b).

    3. The signature for equality is ={(individual individual)atomic}.
    4. The frame signature, ->, is ->{(individual individual individual)atomic}.

      Note that this allows frame terms to occur as arguments to an external predicates or functions, since external symbols can take terms of type atomic as arguments.

    5. The membership signature, #, is #{(individual individual) ⇒ atomic}.

      Note that this permits membership terms as arguments to external predicates or functions.

    6. The signature for the subclass relationship is ##{(individual individual)atomic}.

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

    7. Assignment of signatures to symbols:
      • Each non-datatype symbol in Const, including rif:iri and rif:local symbols, has the signatures individual, atomic, plus, possibly, either p or efp (but not both).

        Thus, a symbol can represent either a function, or a predicate, and it can be an individual or a proposition. Additional restrictions, below, guarantee that symbols with signature efp can occur only as external functions and the same symbol cannot occur both as an external predicate and a normal predicate.

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

    RIF-CASPD uses no special syntax for declaring signatures. Instead, the rule author specifies signatures contextually. That is, since RIF-CASPD 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-CASPD language, and individual, atomic, p, efp, etc., are not reserved keywords.

  4. Supported types of terms.
  5. No aggregate terms or remote term references are allowed.
  6. Required symbol spaces.

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

  7. Supported formulas.

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

    • RIF-CASPD condition

      A RIF-CASPD 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-CASPD rule

      A RIF-CASPD 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, a negated atomic formula, a conjunction of such formulas, or a disjunction of such conjunctions.

        Note that allowing disjunctions of conjunctions in rule conclusions is not a mere syntactic sugar. A rule with (possibly negated) atomic formulas in the conclusion can be equivalently rewritten into a set of rules with singleton (possibly negated) atomic formulas in the conclusions. However, if a conjunction is embedded in a disjunction, such rewriting is not always possible.

        Also note that if a rule conclusion is a disjunction of (possibly negated) atomic formulas, one can eliminate Naf from the conclusion through rewriting [IS98].

      • 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-CASPD condition.

        A RIF-CASPD rule can have free (non-quantified) variables. These are assumed by the RIF-CASPD semantics to be implicitly universally 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-CASPD constraint

      This is a RIF-FLD constraint of the form :- φ, where φ is a RIF-CASPD condition or a universally quantified such constraint.

    • RIF-CASPD fact

      A RIF-CASPD fact is a (optionally universally quantified) disjunction of atomic formulas or negated atomic formulas that do not include Naf. Free variables in such facts are assumed to be implicitly universally quantified.

    • RIF-CASPD group

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

    • RIF-CASPD document

      A RIF-CASPD document is a RIF-FLD document that consists of directives and a RIF-CASPD group formula. There is no Module directive. The Dialect directive must be Dialect("RIF-CASPD"), and the Import(<loc>) directive (with one argument) can import RIF-CASPD documents only. Here loc must be a Unicode character sequence that forms an IRI. There are no CASPD-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-CASPD as a Specialization of RIF-FLD

The semantics of the RIF Core Answer Set Programming 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-CASPD, we need to look at the following parameters:

3.1 Intended Models

The semantics of ASP is typically defined with respect to Herbrand interpretations [CL73], so, we will limit our attention to Herbrand RIF-FLD semantic structures of the form   I = <TV, DTS, HD, IC, IV, IF, INF, Ilist, Itail, Iframe, Isub, Iisa, I=, Iexternal, Iconnective, Itruth>.

In what follows, we will be calling any variable-free term a ground term.

Definition (Intended Models - General). Let Γ be a RIF-CASPD document and Γ* be its ground instantiation. We say a RIF-CASPD 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-CASPD documents.    ☐

To define intended models for ground documents, we need to introduce the following notion of a program quotient (sometimes also called Gelfond-Lifshitz reduction):

Definition (Quotient). Let Γ be a ground RIF-CASPD document and Î a RIF-CASPD semantic multi-structure for it. The quotient of Γ with respect to Î, denoted Γ/ Î is a RIF-CASPD document obtained as follows:

  1. For every rule, constraint, or fact in Γ, replace every negated atomic formula of the form Naf φ with its truth value TValI(Naf φ).
  2. Since the premises and conclusions of the rules, facts, and constraints are composed using disjunctions and conjunctions, we can simplify them using the usual laws of propositional logic. For instance, t can be deleted from every conjunction and f from every disjunction. Conjunctions that contain f can be replaced by f and disjunctions that contain t can be replaced with t.
  3. Remove every rule whose conclusion has been simplified to t or whose premise has been simplified to f. Likewise, remove the facts that have been simplified to t and constraints whose premises have been simplified to f.
  4. 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.    ☐

Intended models of ground RIF-CASPD documents are now defined as follows.

Definition (Intended Models - Ground). Let Γ be a ground RIF-CASPD document. A RIF-CASPD semantic multi-structure Î of Γ is said to be an intended model of Γ if it is a minimal model of the quotient Γ/ Î.    ☐

Note that RIF-CASPD documents might not have any intended models. The smallest example that illustrates this issue is

Group (
      ex:p :- Naf ex:p
)
    

Another reason why intended models might not exist is the consistency requirement. For instance,

Group (
      ex:p
      Neg ex:p
)
    

has no intended models, since ex:p and Neg ex:p cannot be both true in RIF-CASPD semantic structures.

Example 3 (Intended and unintended models)

The ground instantiation of the constraint

Forall ?X1 ?X2 ?Y ?N (
      :- And ( su:coordinates(?X1 ?Y) su:coordinates(?X2 ?Y)
               su:position(?N ?X1 ?Y) su:position(?N ?X2 ?Y) 
               Naf ?X1 = ?X2 )
)
    

from Example 1 (Sudoku), contains, among others, the following constraints:

:- And ( su:coordinates(1 1) su:coordinates(1 1)
	 su:position(1 1 1)  su:position(1 1 1) 
	 Naf 1 = 1 )
    

and

:- And ( su:coordinates(2 1) su:coordinates(1 1)
	 su:position(1 2 1)  su:position(1 1 1) 
	 Naf 2 = 1 )
    

Consider a semantic multi-structure Î where TValÎ(su:coordinates(1 1)) = TValÎ(su:coordinates(1 2)) = TValÎ(su:coordinates(2 1)) = TValÎ(su:coordinates(2 2)) = t and TValÎ(su:position(1 1 1)) = TValÎ(su:position(1 2 1))= t. This means that (1 1) and (2 1) are valid coordinates, that (1 1 1) and (1 2 1) are valid positions, and that 1 is placed at locations (1 1) and (2 1). This is not a valid solution to the Sudoku puzzle as 1 appears twice in the first row. Indeed, as TValÎ(Naf 1 = 1) = f and TValÎ(Naf 2 = 1) = t, the quotient of these two constraints yields the constraint

:- And ( su:coordinates(2 1) su:coordinates(1 1)
         su:position(1 2 1)  su:position(1 1 1) )
    

The body of this constraint is true in Î, which means that Î violates the constraint and is not an intended model of our Sudoku rules.

On the other hand, a multi-structure such that TValÎ(su:coordinates(1 1)) = TValÎ(su:coordinates(1 2)) = TValÎ(su:coordinates(2 1)) = TValÎ(su:coordinates(2 2)) = t and TValÎ(su:position(1 1 1)) = TValÎ(su:position(1 2 2))= t is an intended model.

4 The XML Serialization of RIF-CASPD 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-CASPD formulas, χfld becomes the CASPD-to-XML mapping χcaspd. In this way, the XML serialization of RIF-CASPD is a specialization of the RIF-FLD XML Serialization Framework defined in [RIF-FLD].

5 RIF-CASPD 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 CASPDT,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.