W3C

RIF Core Answer Set Programming Dialect

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 [GLi02] (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.

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 programs 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 that are supported by 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. 

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)
          su:position(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 functions, predicates, and external functions and predicates
      • Predicate signature for non-external symbols p. This signature has the arrow expressions for positional functions and 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, ..., sk ∈ ArgNames.
      • External function or predicate signature efp. This signature has the following arrow expressions, where Τ can be either individual or atomic: () ⇒ Τ, (Τ) ⇒ Τ, (Τ Τ) ⇒ Τ, ..., plus (s1->Τ ... sk->Τ) ⇒ Τ, for all k>0 and all s1, ..., sk ∈ ArgNames.
    3. The signature for equality is ={(individual individual) ⇒ atomic}.
    4. The frame signature, ->, is ->{(individual individual individual) ⇒ atomic}.

      Note that this allows for the possibility that a frame term might occur as an argument to a predicate, a function, or inside some other term.

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

      Note that this allows for the possibility that a membership term might occur as an argument to a predicate, a function, or inside some other term.

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

      As with frames and membership terms, this allows for the possibility that a subclass term might occur inside some other term.

    7. Assignment of signatures to symbols:
      • Non-datatype symbols in Const, including the rif:iri and rif:local:
        • Either have the signatures individual, atomic, and p.
        • Or the signature efp.

        Thus, a symbol can represent either an external function or predicate, or it is a regular symbol. In the latter case, it can appear in the position of an individual, a function, or a predicate without any restrictions.

      • 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, and term are not reserved keywords.

  4. Supported types of terms.
  5. No aggregate terms, module terms, or formula terms are allowed. (In RIF-FLD, formula terms correspond to compound formulas that involve logical connectives and quantifiers.)
  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):

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 domains [CL73], and since RIF-CASPD does not have non-external function symbols the domain is particularly simple in that case. Namely, we will limit our attention to RIF-FLD semantic structures   I = <TV, DTS, D, IC, IV, IF, INF, Ilist, Itail, Iframe, Isub, Iisa, I=, Iexternal, Iconnective, Itruth>  that all have the same domain, which consists of the set of all constant symbols that belong to the symbol spaces in DTS. The mapping IC, which maps constants to the elements of the domain D is also the same for all intended structures: it is simply the identity mapping. Note that the mappings Ilist and Itail can be left unspecified in RIF-CASPD, as the syntax of this dialect does not permit list terms.

Note that according to the definition of truth valuation in RIF-FLD, TValI(φ) = t if and only if TValI(Naf φ) = f. However, RIF-FLD imposes no any such constraint for Neg φ. However, in RIF-CASPD we impose the following weaker requirement on the intended structures:

RIF-FLD semantic multi-structures that are built out of semantic structures over Herbrand domains and that satisfy the above restriction will be called RIF-CASPD semantic multi-structures.

Definition (Ground Instantiations). Let Γ be a RIF-CASPD document. Its ground instantiation is a RIF-CASPD document obtained from Γ by replacing every RIF-CASPD rule, fact, or constraint in Γ with the set of all their ground instances.
A rule, fact, or constraint φ is said to be a ground instance of another rule, fact, or constraint, ψ if and only if φ is obtained from ψ by a consistent replacement of variables with constant symbols. Consistency here means that, while constructing φ from ψ, the same variables are always substituted with the same constants.    ☐

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

We also need to define minimal RIF-CASPD models.

Definition (Minimal Model). Let Γ be a ground RIF-CASPD document. A RIF-CASPD semantic multi-structure Î of Γ is said to be a minimal model of Γ if for every other RIF-CASPD model Î' of Γ the following holds:

for every formula φ of the form L or Neg L, where L is a ground atomic formula.    ☐

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 Γ/ Î.    ☐

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.