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 [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] ) ) ) )
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 for the possibility that a frame term might occur as an argument to a predicate, a function, or inside some other term.
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.
As with frames and membership terms, this allows for the possibility that a subclass term might occur inside some other term.
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.
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.
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.
Combined with the fact that in a well-formed term of the form External(t) the subterm t must be an instantiation of an external schema (by the definition of well-formed external terms in RIF-FLD), it follows that a predicate or a function symbol, p, that occurs in an external term External(p(...)) cannot also occur as a non-external symbol.
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, and a negated (normal or external) atomic formula, 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 to be implicitly universally quantified by the RIF-CASPD semantics.
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.
A RIF-CASPD group is a RIF-FLD group 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 order <_{t} is total.
RIF-CASPD supports the datatypes listed in Section Datatypes of [RIF-DTB].
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 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.
Note that according to the definition of truth valuation in RIF-FLD, TVal_{I}(φ) = t if and only if TVal_{I}(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:
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:
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:
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.
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