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 |
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] ) ) ) )
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.
All extension points of RIF-FLD are removed (specialized by replacing them with zero objects).
The alphabet of the RIF-CASPD presentation syntax is identical to the alphabet of RIF-FLD.
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:
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.
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.
Note that this permits membership terms as arguments to external predicates or functions.
As with frames and membership terms, this allows subclass terms to occur inside other external terms.
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.
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.
Note that lists are not supported. (Some ASP systems do support lists, but we leave this feature out of the core.) Also, the signatures limit the language so that function terms are allowed only for externally defined functions.
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.
It thus follows that function symbols are allowed only in case of built-in and external functions.
RIF-CASPD requires the symbol spaces defined in Section Constants, Symbol Spaces, and Datatypes of [RIF-DTB].
RIF-CASPD supports the following types of formulas (see Well-formed Terms and Formulas in [RIF-FLD] for the definitions):
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.
A RIF-CASPD rule is a RIF-FLD rule implication or a universally quantified RIF-FLD rule with the following restrictions:
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].
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)).
This is a RIF-FLD constraint of the form :- φ, where φ is a RIF-CASPD condition or a universally quantified such constraint.
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.
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.
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.
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:
The restrictions on the signatures of symbols, terms, or formulas in RIF-CASPD do not affect the semantic definitions of RIF-FLD in any significant way.
The set TV of truth values in RIF-CASPD consists of two values, t and f, such that f <_{t} t.
The set of data types and DTS of RIF-CASPD 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.
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-CASPD, this set is defined in Section 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, 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}>.
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:
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.
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].
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 CASPD_{T,E} producers and consumers.
TBD