\documentclass[12pt]{article} \usepackage{latexsym} \usepackage{amssymb} \usepackage{url} %----------- dimensions and where on page ----------- %For portrait \textwidth 6.0in \textheight 8.2in \hoffset=-.25in \voffset=-0.2in %For landscape %\textwidth 8.0in %\textheight 6.0in %\hoffset=0.3in %\voffset=-0.2in %--------- other numeric parameters ------------------ \parskip=.1in %++++++++++ END ++++++++++++++++++++++++++++++++++++++ \begin{document} \begin{center} {\LARGE\bf Answer-Set Programming: a Declarative Knowledge Representation Paradigm } \ \\ {\Large ESSLLI'2001 --- Logic and Computing: an introductory course \ \\ \ \\ \ \\ {\em Ilkka Niemel\"a}\\ Helsinki University of Technology\\ Department of Computer Science and Engineering\\ Laboratory for Theoretical Computer Science\\ P.O.Box 5400, FIN-02015 HUT, Finland \url{http://www.tcs.hut.fi/~ini/}\\ e-mail: {\tt Ilkka.Niemela@hut.fi} \ \\ \ \\ {\em Miros\l aw Truszczy\'nski}\\ Department of Computer Science\\ University of Kentucky \\ Lexington, KY 40506--0046\\ \url{http://www.cs.engr.uky.edu/~mirek/}\\ e-mail: {\tt mirek@cs.uky.edu} } \end{center} \newpage \section{Overview} The area of nonmonotonic reasoning originated about twenty years ago \cite{re78,mca80,re80,mcdd80} in response to challenges of knowledge representation and, more general, artificial intelligence. Commonsense reasoning, defeasible inferences, belief revision and formalizations of the frame problem seemed to require a different framework than that offered by first-order logic. As a result, nonmonotonic logics were proposed: default logic by Reiter \cite{re80}, modal nonmonotonic logics by McDermott and Doyle \cite{mcdd80,mcd82} and Moore \cite{mo85}, and circumscription by McCarthy \cite{mca80}. In about the same time, Horn logic programming was proposed by Kowalski as an alternative, declarative as opposed to procedural, programming paradigm \cite{ko74,ko79}. Horn logic programming offered a promise of an easy program development and verification. But with negation in the syntax, it was no longer clear what the semantics is. The problem was successfully addressed in the late 80s with the emergence of the stable model semantics by Gelfond and Lifschitz \cite{gl88}, well-founded semantics by Van Gelder, Ross and Schlipf \cite{vrs91}, and some other related semantics capturing aspects of the intuition of the negation as failure. There are strong connections between logic programming with negation and nonmonotonic reasoning. For one, stable model semantics is nonmonotonic itself. Secondly, logic programming with stable model semantics can be viewed as a fragment of default logic \cite{mt89c,bf91a}. In fact, logic programming with stable model semantics for a number of years now has been regarded as a computational embodiment of nonmonotonic reasoning and a candidate for an effective knowledge representation tool. How to actually process logic programs under stable model semantics and how to interpret them has been, however, less clear. The stable model semantics seemed to be at odds with the traditional logic programming paradigm of a single intended model. In the late 90s several implementations of algorithms for computing stable models of logic programs and disjunctive logic programs were proposed \cite{ns96,Simons2000:phd,ns00,elmps97,elmps98}. And, as they were studied, it became clear that they are instantiations of a different programming paradigm than that of standard logic programming. This new paradigm has been formally identified in the late 90s and has since become known as Answer-Set Programming (or ASP, for short) \cite{mt99,nie99,li99b}. Answer-set programming is a paradigm in which programs are built as theories in some formal system $\cal F$ with a well-defined syntax, and with a semantics that assigns to a theory $P$ in the system a {\em collection} of subsets of some domain. These subsets are referred to as {\em answer sets} of $P$ and specify the results of computation based on $P$. To solve a problem $\Pi$ in an ASP formalism, we find a program $P$ so that the solutions to $\Pi$ can be reconstructed in polynomial time from the answer sets to $P$. What are the benefits of ASP over traditional logic programming approaches? We believe that the major advantage of ASP is its simplicity and connection to constraint programming. There are no function symbols, and there is no need for resolution or unification (at least in the present implementations; this situation may change as the field develops). The role of recursion is dramatically restricted. Essentially, the only recursion that is needed is that required by transitive closure specification. Clauses and programs are viewed as {\em constraints} on sets. Programs are developed by representing problem constraints in a direct and straightforward fashion. Further, most ASP formalisms have their roots in default logic or other similar nonmonotonic logics. Consequently, modeling incomplete information, defeasible reasoning and such phenomena as the frame problem become quite easy. Finally, there is some formal and experimental evidence that domain or problem representations using ASP formalisms based on nonmonotonic logics lead to more concise programs. Conciseness of representations is important as it might lead to significant speed up in processing times. Ease of modeling and program development is important as it may determine whether the approach will become widely accepted. In recent years it became evident that answer-set programming formalisms can also be built on top of propositional satisfiability checkers and their extensions \cite{et00a}. The logic PS+ and its implementation, system {\em aspps} \cite{et01a}, is an illustration of this approach. Answer-set programming is a new development. It is too early to say definitely whether it will make any significant impact on the practice of declarative programming and practical knowledge representation. There are, however, strong indications that it will. Its theoretical foundations are well understood, including complexity and expressive power. It is applicable to a wide range of search and decision problems. It is closely related to constraint programming. Last but not least, there are already promising implementations. \newcommand{\Smodels}{\texttt{Smodels}} \section{Applications} %A short text mentioning all main areas of applicability of the approach %and listing all relevant references (those listed after end{document} %statement and, possibly, some new ones). TO BE DONE BY ILKKA We briefly review interesting areas where ASP systems have already been used. \begin{itemize} \item Planning Planning was one of the main areas that motivated the development of nonmonotonic reasoning systems and the use of ASP in this area has been studied by a number of researchers, see e.g.~\cite{DNK97,li99b,nie99,Parmar2001:asp,TB2001:asp,SBM2001:asp}. An interesting example of an advanced project is research at Texas Tech University on developing a decision support system for the flight controllers of space shuttles using the ASP approach~\cite{BBGBW2001:padl}. \item Product configuration General methodology for product configuration using ASP techniques has been developed~\cite{SN99:padl,SNTS2000:ecai,SNTS2001:asp} and interesting application projects have been started, see e.g.~the WeCoTin project (\url{http://www.soberit.hut.fi/WeCoTin/}). Research on software configuration using ASP~\cite{Syrjanen2000:cl,Syrjanen2000:ecai} has been employed to develop a prototype configurator for the complete Debian Linux system distribution~\cite{Syrjanen99:dtyo}. \item Computer aided verification ASP has been used for a variety of key inference tasks in computer aided verification. The \Smodels\ system has been employed as an inference engine in a model checker~\cite{LRS98:tacas}. An analysis method for Petri nets based on finite complete prefixes has been built on top of \Smodels~\cite{Heljanko:Fundamenta99,Heljanko99:csp,EspHel:SPIN2001}, see the \texttt{mcsmodels} and \texttt{unfsmodels} tools (\url{http://www.tcs.hut.fi/~kepa/tools/}). Similarly, it has been used in a stubborn set reduction method for Petri net reachability analysis~\cite{Varpaaniemi2000:fi}, see the \texttt{prod} tool (\url{http://www.tcs.hut.fi/Software/prod/}). Recently, a symbolic model checking method for asynchronous systems based on bounded model checking techniques and ASP has been developed~\cite{HN2001:asp,HN2001:lpnmr}. \end{itemize} There are a number other interesting areas where ASP methodology has been employed including dynamic constraint satisfaction~\cite{SGN99:cp}, wire routing~\cite{ELW2000:cl,ET2001:asp}, network management~\cite{SL2001:asp}, feature interaction~\cite{AAR99,AABR2000}, logical cryptanalysis~\cite{HMN2000:nmr}, security protocol analysis~\cite{AM2000}, network inhibition analysis~\cite{Aura2000}, diagnosis~\cite{GG2001:asp}, and computation of (total and partial) stable models for disjunctive programs~\cite{JNSY2000:kr}. \section{Where to get the software?} \label{sites} This tutorial discusses knowledge representation tools based on a new computational paradigm of Answer Set Programming (ASP). ASP has its roots in nonmonotonic reasoning and, especially, in logic programming with negation under the stable model semantics. There are several implementations of this paradigm. The two discussed in the tutorial are {\em smodels} and {\em aspps}. The former has been developed in Helsinki University of Technology in the group led by Ilkka Niemel\"a. The latter has been developed in the University of Kentucky by Deborah East and Miros\l aw Truszczy\'nski. Two other well advanced ASP systems are {\em dlv} and {\em ccalc}. The {\em dlv} system has been developed at the Technical University of Vienna by Nicola Leone, Thomas Eiter and their collaborators. The {\em ccalc} system has been developed at the University of Texas at Austin by Norm McCain and is now being maintained by Texas Action Group. Yet another system of interest is {\em ldl++} developed by Natraj Ami and Kayliang Ong at MCC (with technical guidance from Carlo Zaniolo). The urls for all these systems are given below. \ \\ \ \\ {\em smodels}: \url{http://www.tcs.hut.fi/Software/smodels/}\\ {\em aspps}: \url{http://www.cs.engr.uky.edu/ai/aspps/}\\ {\em dlv}: \url{http://www.dbai.tuwien.ac.at/dlv/}\\ {\em ccalc}: \url{http://www.cs.utexas.edu/users/tag/cc/}\\ {\em ldl++}: \url{http://www.cs.ucla.edu/ldl/} \section{Example programs} In this section we present programs for solving several logic puzzles, combinatorial problems and planning problems. We start by providing problem statements. Then, we present {\em smodels} and, later, {\em aspps} programs for these problems. \subsection{Problems} \paragraph*{Missionaries and cannibals.} There are three cannibals and three missionaries on the left bank of a river. They have a boat. The boat has capacity 2. If at any time there are more cannibals than missionaries on either bank, the cannibals eat the missionaries. The goal is to arrange the way of moving all 6 of them to the right bank. The problem of missionaries and cannibals is a classic AI puzzle that received quite a lot of attention \cite{lif00}. \paragraph*{15-puzzle.} A $4\times 4$ grid is filled with 15 movable tiles labeled $1,\ldots,15$. One square is left blank. Tiles can be rearranged by moving a tile into a blank square (assuming the two locations share an edge). The goal is to rearrange the tiles so that they are arranged from 1 to 15 in the {\em row-major} order, with the blank square occupying the left top corner. The 15-puzzle problem is a hard search problem \cite{korf00}. \paragraph*{Blocks-world planning.} Blocks are arranged in stacks on the floor. Each block is located on exactly one block or on the floor. No two blocks are placed on the same block. A block that is on top of its stack can be moved and placed on the top of another stack or on the floor. Find a plan (a sequence of actions) to rearrange the blocks into a desired final configuration. Both sequential (only one block moved in a step) and concurrent (allows for several blocks to be moved in the same step) versions are of interest. This is a classic planning problem in AI. \paragraph*{$n$-queens problem.} Given n $n\times n$ chessboard, the goal is to place on it $n$ queens so that no two queens attack each other (that is, no two queens are in the same row, column or in the same diagonal). The $n$-queens problem is often used in testing constraint solvers. \paragraph*{Hamilton cycle problem.} Given a directed graph $G$, find a cycle in $G$ that goes through all vertices of the graph exactly once (if such a cycle exists). The Hamilton-cycle problem is a classic NP-complete graph problem. \paragraph*{Vertex-cover problem.} A set of vertices of an undirected graph is called a {\em vertex cover} if every edge in the graph has at least one of its ends in the set. The problem is, given an undirected graph $G$ and an integer $k$, to compute a vertex cover of $G$ with no more than $k$ vertices (if such a cover exists). The vertex-cover problem is another classic NP-complete problem. It is also a difficult test problem for search algorithms. \paragraph*{Schur numbers.} A set $A$ of integers is sum-free if for every $x,y\in A$ (not necessarily distinct), $x+y\notin A$. The Schur number $S(k)$ is defined as the smallest integer $n$ such that the set $\{1,2,\ldots,n\}$ {\bf cannot} be partitioned into $k$ parts so that each part is sum-free. \subsection{{\em Smodels} programs} A typical command line for the smodels systems is of the form \noindent \verb+lparse [options] file1 file2 | smodels m + \noindent Typical options are '-c const=n' to set a constant appearing in the program and '-dn' for eliminating all domain predicates while doing grounding in order to reduce the size of the grounded program. The integer $m$ gives the number of models that need to be found (default is one and '0' means all models). Hence, a command line for the Missionaries and cannibals encoding presented next could be the following \noindent \verb+lparse -dn -c n=11 mc.lp | smodels 0 + \noindent where the constant $n$ is set to '11' and \emph{smodels} is instructed to find all stable models. \paragraph{Missionaries and cannibals.} The two key predicates are {\em state} and {\em move}. Atom $state(CC,MM,B,T)$ is read as follows: at time $T$ there are $CC$ cannibals and $MM$ missionaries on the left bank. $B=1$ means that the boat is on the left bank, $B=0$ means that the boat is on the right bank. Atom $move(C,M,T)$ means that at time $T$, $C$ cannibals and $M$ missionaries are moving to the opposite bank of the river (the direction depends on the location of the boat). \begin{verbatim} % Domain predicates time(0..n). % specifies time range (number of moves) % in which the solution is to be found number(0..3). % specifies allowed number of cannibals % (or missionaries) on a bank boatcap(0..2). % specifies allowed numbers of % people in the boat % Initial state: % 3 cannibals and 3 missionaries on the left (1) % bank of the river at time 0. state(3,3,1,0). % Define safe states safestate(CC,MM) :- number(CC;MM), MM==0. safestate(CC,MM) :- number(CC;MM), MM>=CC. % Select a valid move at time T, given the current state good1(CC,MM,C,M) :- boatcap(C;M), number(CC;MM), time(T), 1 <= C+M, C+M <= 2, C <= CC, M <= MM, safestate(CC-C,MM-M), safestate(3-CC+C,3-MM+M). 1 { move(C,M,T): boatcap(C): boatcap(M): good1(CC,MM,C,M)} 1 :- time(T), number(CC;MM), state(CC,MM,1,T), not goal(T). good0(CC,MM,C,M) :- boatcap(C;M), number(CC;MM), time(T), 1 <= C+M, C+M <= 2, C <= 3-CC, M <= 3-MM, safestate(CC+C,MM+M), safestate(3-CC-C,3-MM-M). 1 { move(C,M,T): boatcap(C): boatcap(M): good0(CC,MM,C,M)} 1 :- time(T), number(CC;MM), state(CC,MM,0,T), not goal(T). % Compute the next state state(CC-C,MM-M,0,T+1) :- number(CC;MM), boatcap(C;M), time(T), state(CC,MM,1,T), move(C,M,T). state(CC+C,MM+M,1,T+1) :- number(CC;MM), boatcap(C;M), time(T), state(CC,MM,0,T), move(C,M,T). % Determine whether the goal has been reached at time T goal(T) :- time(T), state(0,0,0,T). % Determine that the goal was reached ok :- time(T), goal(T). % Eliminate all plans which do not lead to the goal :- not ok. \end{verbatim} \paragraph{15-puzzle.} The key predicate are \emph{move} and \emph{in}. Atom \emph{move(T,X,Y)} has the meaning: at time $T$ tile 0 is moved to location \emph{(X,Y)} and \emph{in(T,X,Y,A)} is read as: at time $T$ tile A is in location \emph{(X,Y)}. Initial configuration is give as facts \emph{in0(x,y,a)}. \begin{verbatim} % An example initial configuration % 12 moves required % 1 5 2 7 % 4 0 3 11 % 8 9 6 15 % 12 13 10 14 in0(1,1,1). in0(1,2,5). in0(1,3,2). in0(1,4,7). in0(2,1,4). in0(2,2,0). in0(2,3,3). in0(2,4,11). in0(3,1,8). in0(3,2,9). in0(3,3,6). in0(3,4,15). in0(4,1,12). in0(4,2,13). in0(4,3,10). in0(4,4,14). % Domain predicates time(0..t). pos(1..4). entry(0..15). % Select where to move tile 0 { move(T,X,Y) } :- time(T), T < t, pos(X;Y;X1;Y1), in(T,X1,Y1,0), abs(X-X1) + abs(Y-Y1) == 1. % Only one move at a time allowed :- 2 { move(T,X,Y):pos(X):pos(Y) }, time(T), T< t. % For every time there must be a move :- { move(T,X,Y):pos(X):pos(Y) } 0, time(T), T< t. % Effects of a move % Define the moving tile for each time T moving(T,A) :- time(T), T < t, pos(X;Y), entry(A), move(T,X,Y), in(T,X,Y,A). % The moving tile A is moved to the location of tile 0 in(T+1,X,Y,A) :- time(T), T < t, pos(X;Y), entry(A), moving(T,A), in(T,X,Y,0). % Tile 0 is moved to the location (X,Y) when doing move(T,X,Y) in(T+1,X,Y,0) :- time(T), T < t, pos(X;Y), move(T,X,Y). % Frame axiom in(T+1,X,Y,A) :- time(T), T < t, entry(A), pos(X;Y), A != 0, in(T,X,Y,A), not moving(T,A). % An example of a pruning rule % Do not undo the last move :- time(T), T < t-2, pos(X;Y), in(T,X,Y,0), in(T+2,X,Y,0). % Goal configuration % 0 1 2 3 % 4 5 6 7 % 8 9 10 11 % 12 13 14 15 in_t(1,1,0). in_t(1,2,1). in_t(1,3,2). in_t(1,4,3). in_t(2,1,4). in_t(2,2,5). in_t(2,3,6). in_t(2,4,7). in_t(3,1,8). in_t(3,2,9). in_t(3,3,10). in_t(3,4,11). in_t(4,1,12). in_t(4,2,13). in_t(4,3,14). in_t(4,4,15). % Goal configuration must be satisfied :- entry(A), pos(X), pos(Y), in(t,X,Y,A), not in_t(X,Y,A). :- entry(A), pos(X), pos(Y), not in(t,X,Y,A), in_t(X,Y,A). % Initial configuration in(0,X,Y,A) :- in0(X,Y,A). \end{verbatim} \paragraph{Blocks-world planning.} The key predicates are \emph{moveop} and \emph{on}. Atom \emph{move(X,Y,T)} has the meaning: at time $T$ block X is moved on top of object Y and \emph{on(X,Y,T)} is read as: at time $T$ block $X$ is on object $Y$. Initial conditions include facts about the blocks and \emph{on} predicate and a goal rule. \begin{verbatim} % An example of initial and goal conditions % Blocks block(a). block(b). block(c). % b % a c % Initial configuration % b c a on(a,b,0). on(b,table,0). on(c,table,0). % ------- % Initial Goal % Goal conditions goal(T) :- time(T), on(b,c,T), on(c,a,T). % Domain predicates time(0..n). nextstate(Y,X) :- time(X), time(Y), Y = X + 1. % Auxiliary predicates object(table). object(X) :- block(X). covered(X,T) :- block(Z), block(X), time(T), on(Z,X,T). on_something(X,T) :- block(X), object(Z), time(T), on(X,Z,T). available(table,T) :- time(T). available(X,T) :- block(X), time(T), on_something(X,T). % Select a moveop provided that preconditions hold { moveop(X,Y,T) } :- time(T), block(X), object(Y), X != Y, on_something(X,T), available(Y,T), not covered(X,T), not covered(Y,T). % Operator effects: on(X,Y,T2) :- block(X), object(Y), nextstate(T2,T1), moveop(X,Y,T1). % Frame axioms on(X,Y,T2) :- block(X), object(Y), nextstate(T2,T1), on(X,Y,T1), not moving(X,T1). moving(X,T) :- time(T), block(X), object(Y), moveop(X,Y,T). % Concurrent moveop instances are allowed % A block cannot be moved to two destination :- 2 { moveop(X,Y,T):object(Y) }, block(X), time(T). % The destination cannot be moving :- block(X), object(Y), time(T), moveop(X,Y,T), moving(Y,T). % No two blocks moved onto the same block :- 2 { moveop(X,Y,T):block(X) }, block(Y), time(T). % Exclude models where the goal has not been reached. :- not goal. goal :- time(T), goal(T). goal(T2) :- nextstate(T2,T1), goal(T1). % Optimizations % Stop when the goal has been reached :- block(X), object(Y), time(T), moveop(X,Y,T), goal(T). % No move from table to table :- block(X), time(T), moveop(X,table,T), on(X,table,T). % No move on something and then to table :- nextstate(T2,T1), block(X), object(Y), moveop(X,Y,T1), moveop(X,table,T2). \end{verbatim} \paragraph{$n$-queens problem.} Domain predicate $\mathit{d}$ specifies the number of queens and the dimensions of the board. The main predicate is the predicate $\mathit{q}$. Atom $\mathit{q}(X,Y)$ represents the fact that there is a queen in the position $(X,Y)$. \begin{verbatim} % Domain predicate: the dimension of the board. d(1..n). % Exactly one queen in each row 1 { q(X,Y):d(Y) } 1 :- d(X). % Exactly one queen in each column 1 { q(X,Y):d(X) } 1 :- d(Y). % No two queens on an diagonal :- d(X;Y;X1;Y1), q(X,Y), q(X1,Y1), X < X1, Y != Y1, abs(X - X1) == abs(Y - Y1). \end{verbatim} \paragraph{Hamilton cycle problem.} The graph is given as facts $\mathit{vtx(X)}$ and $\mathit{edge(X,Y)}$ and one vertex v is given as initial vertex $\mathit{initialvtx(v)}$. The key predicate is $\mathit{hc}$. Atom $\mathit{hc}(X,Y)$ represents the fact that edge $(X,Y)$ is in the Hamiltonian cycle to be constructed. \begin{verbatim} % Select edges for the cycle { hc(X,Y) } :- edge(X,Y). % Each vertex has at most one incoming edge in a cycle :- 2 { hc(X,Y):edge(X,Y) }, vtx(Y). % Each vertex has at most one outgoing edge in a cycle :- 2 { hc(X,Y):edge(X,Y) }, vtx(X). % Every vertex must be reachable from the initial vertex through chosen % hc(v,u) edges :- vtx(X), not r(X). r(Y) :- hc(X,Y), edge(X,Y), initialvtx(X). r(Y) :- hc(X,Y), edge(X,Y), r(X), not initialvtx(X). \end{verbatim} \paragraph{Vertex-cover problem.} The graph is given as facts $\mathit{vtx(X)}$ and $\mathit{edge(X,Y)}$ and $k$ is the upper bound for vertices in a cover. The main predicate is $\mathit{incover}$. Atom $\mathit{incover}(X)$ represents the fact that vertex $X$ is in a vertex cover. \begin{verbatim} % Select at least one of the ends of an edge to be included in the cover 1 { incover(X), incover(Y) } :- edge(X,Y). % Eliminate models where k+1 or more vertices have been chosen :- k+1 {incover(X):vtx(X) }. \end{verbatim} \paragraph{Schur numbers.} The range of integers to be partitioned is $n$ and the number of parts is $k$. The main predicate is $\mathit{inpart}$. Atom $\mathit{inpart}(X,P)$ represents the fact that number $X$ is included in part $P$. The idea is to find a partition of integers {1,2,...,n} into k parts such that each part is sum free, i.e. for any $X$ and $Y$, $X$ and $X+X$ are in different parts and if $X$ and $Y$ are in the same part, then $X+Y$ is in a different part. \begin{verbatim} % Domain predicates number(1..n). part(1..p). % Assign each integer to exactly one part. 1 { inpart(X,P):part(P) } 1 :- number(X). % X and X+X cannot be in the same part :- number(X), part(P), inpart(X,P), inpart(X+X,P). % X, Y, and X+Y cannot be in the same part :- number(X;Y), X != Y, part(P), inpart(X,P), inpart(Y,P), inpart((X+Y),P). % Remove some symmetries by taking always the lowest free part :- number(X), part(P), inpart(X,P), part(P1), P1 < P, not occupied(X,P1). % occupied(X,P) iff there is a number Y < X in P occupied(X,P) :- number(X;Y), part(P), Y < X, inpart(Y,P). \end{verbatim} \subsection{{\em aspps} programs} Each program consists of two files: the {\em data} file ({\tt data}) and the {\tt rule} file ({\tt rules}). In each case, we start by producing a ground version of the program. To this end we run the {\tt grnd} program as follows: \begin{verbatim} grnd -c t1=k1 t2=k2 -d data -r rules \end{verbatim} Here $t1$ and $t2$ are two constants appearing in the program whose values (say, $k1$ and $k2$) are entered at the command line when invoking {\tt grnd}. If necessary, more constants can be specified in this way. The program {\tt grnd} produces a ground version of the program that is stored in the file {\tt k1\_k2\_data\_rules}. To find answer sets we run the program {\tt aspps}. Its input is the file {\tt k1\_k2\_data\_rules} produced by {\tt grnd}. \begin{verbatim} aspps -f k1_k2_data_rules \end{verbatim} Option -S followed by a list of predicates, prints out all the ground atoms in the solution that are built of predicates on the list. For instance, \begin{verbatim} aspps -f k1_k2_data_rules -S p1 p2 \end{verbatim} lists all ground atoms built of predicates $p1$ and $p2$ that belong to a solution found by {\tt aspps}. No output is produced if no solutions were found. A more detailed description of the programs {\tt grnd} and {\tt aspps} is available at the website given in Section \ref{sites}. \paragraph*{Missionaries and cannibals.} \noindent Data file. \begin{verbatim} time[0..t]. % specifies time range (number of moves) in % which the solution is to be found num[0..3]. % specifies allowed number of cannibals (or % missionaries on a bank boat[0..1]. % 0 - boat on the left bank % 1 - boat on the right bank instate(3,3,0). % initial state \end{verbatim} \noindent Rules file. The two key predicates are {\em state} and {\em move}. Atom $state(T,CC,MM,B)$ has the following meaning: at time $T$ there are $CC$ cannibals and $MM$ missionaries on the left bank. $B=0$ means that the boat is on the left bank, $B=1$ means that the boat is on the right bank. Atom $move(T,C,M)$ means that at time $T$, $C$ cannibals and $M$ missionaries are moving to the opposite bank of the river (the direction depends on the location of the boat). \begin{verbatim} % Declare predicates pred state( time , num , num , boat ). pred move( time , num , num ). % Declare variables var time T. var num M,C,MM,CC. var boat B. % At time 0, the state coincides with the initial state given % by the input state(0,CC,MM,B) -> instate(CC,MM,B). % Select a configuration at time T 1{state(T,CC,MM,B):num(CC):num(MM):boat(B)}1. % Select a move for time T T 1{move(T,C,M):num(C):num(M)}1. % No moves at time t (the plan ends at time t) move(t,C,M) -> . % Enforce the boat capacity costraint move(T,C,M) -> M+C<=2. % At least one person must be moving to the other bank move(T,C,M) -> 0 C<=CC. state(T,CC,MM,0),move(T,C,M) -> M<=MM. % If the boat is on the right bank no more than 3-CC cannibals % (this is how many of them ae on the right bank) and no more % than 3-MM missionaries may be chosen to move to the other side state(T,CC,MM,1),move(T,C,M) -> C<=3-CC. state(T,CC,MM,1),move(T,C,M) -> M<=3-MM. % Ensure that a move is not immediately "undone" 0 . % Relate the next state to the previous one and to the % move chosen T state(T+1,CC-C,MM-M,1). T state(T+1,CC+C,MM+M,0). % Eliminate states not safe for the missionaries state(T,CC,MM,B), MM!=0, CC > MM -> . state(T,CC,MM,B), MM!=3, CC < MM -> . % At time t the goal state must be reached state(t,0,0,1). \end{verbatim} \paragraph*{15-puzzle.} See the slides (Section \ref{slides}). \paragraph*{Blocks-world planning.} Data predicate $\mathit{time}$ specifies the time horizon (constant $t$ is entered from the command line). Data predicate block defines the set of blocks (constant $k$ is entered from the command line). Data predicate $\mathit{on0}$ defines the initial configuration. Atom $\mathit{on0(A,B)}$ means that block $A$ is (initially) on block $B$. Similarly, data predicate $\mathit{onF}$ provides a specification for the goal configuration. Atom $\mathit{onF(A,B)}$ means that in the goal configuration block $A$ must be on block $B$. The specification of the goal configuration may be incomplete. The data file given here is the example large.c, proposed by Kautz and Selman (\url{http}). Key program predicates are $\mathit{on}$, $\mathit{move}$ and $\mathit{top}$. Atom $\mathit{on}(T,A,B)$ means that at time $T$ block $A$ is on block $B$. Atom $\mathit{move}(T,A)$ represents the fact that at time $T$, block $A$ is one of the blocks to be moved. Finally, atom $\mathit{top}(T.A)$ means that at time $T$ block $A$ is at the top of its stack of blocks. \noindent Data file. \begin{verbatim} time[0..t]. block[0..15]. % Initial configuration on0(13,0). on0(12,13). on0(1,12). on0(2,1). on0(3,2). on0(15,0). on0(14,15). on0(4,14). on0(5,4). on0(10,5). on0(11,10). on0(6,0). on0(7,6). on0(8,7). on0(9,8). % Partial description of the goal configuration onF(5,10). onF(1,5). onF(14,1). onF(9,4). onF(8,9). onF(13,8). onF(15,13). onF(11,7). onF(3,11). onF(2,3). onF(12,2). \end{verbatim} \noindent Rule file. \begin{verbatim} %% Declare predicates pred on( time , block , block ). pred move( time , block ). pred top( time , block ). %% Declare variables var time T. var block A,B,C. %% Specify an arrangement of blocks at time T % Each block other than the floor is on top of exactly one % block 0 1 { on(T,A,B): block(B) } 1. % Each block other than the floor is either a top block or % is under exactly one block or is the top block 0 1{top(T,A), on(T,B,A): block(B)}1. % floor is never on any other block on(T,0,A) -> . % floor is never a top top(T,0) -> . %% The state at time 0 must coincide with the initial configuration on(0,A,B) -> on0(A,B). on0(A,B) -> on(0,A,B). %% The state at time t must be consistent with the specification %% of the goal onF(A,B) -> on(t,A,B). %% Constraints on moves % Floor never moves move(T,0) -> . % Moved blocks are restricted to top blocks. on(T,B,A), move(T,A) -> . % No move is made at time t. move(t,A) -> . %% A block cannot be moved on top of a block that is being moved %% in the same move move(T,A),move(T,B),on(T+1,A,B) -> . %% No block is directly moved back where it was move(T,A), on(T,A,B), on(T+2,A,B) -> . %% No block moves on the same location it was in move(T,A), on(T,A,B), on(T+1,A,B) -> . %% Compute the new state % None of these constraints is necessary. But when put together % they seem to work best. T 1{on(T+1,A,B), move(T,A)}1. on(T+1,A,B) -> 1{move(T,A), on(T,A,B)}1. \end{verbatim} \paragraph*{$n$-queens problem.} Data predicate $\mathit{number}$ specifies the number of queens and the dimensions of the board. The main predicate is the predicate $\mathit{queen}$. Atom $\mathit{queen}(C,R)$ represents the fact that there is a queen in the position $(C,R)$. \noindent Data file. \begin{verbatim} number[1..n]. \end{verbatim} \noindent Rule file. \begin{verbatim} % Predicate declarations pred queen(number, number). % Variable declarations var number C, R, I. % Exactly one queen in each row 1 { queen(C,R) : number(C) } 1. % Exactly one queen in each column 1 { queen(C,R) : number(R) } 1. % No two queens on an "ascending" diagonal queen(C,R), queen(C+I,R+I) -> . % No two queens on a "descending" diagonal queen(C,R), queen(C+I,R-I) -> . \end{verbatim} \paragraph*{Hamilton cycle problem.} We specify the rule file only. The data file must define the vertex set of the graph (for instance, the statement {\tt vtx[1..n]}) will define the vertex set to be $\{1,\ldots, n\}$, where $n$ is a parameter entered from the command line). The data file must also list all (directed) edges of the graph as facts $\mathit{edge}(a,b)$, where $\mathit{edge}$ is another data predicate. The key program predicate is $\mathit{cycle}$. Atom $\mathit{cycle}(X,Y)$ represents the fact that vertex $Y$ is in position $X$. In other words, the predicate $\mathit{cycle}$ represents a permutation of the vertices of the graph. The permutation represents a Hamilton cycle if for every position $X$, there is an edge between the vertex in position $X$ and the vertex in position $X+1$ (the next position after $n$ is 1). \noindent Rule file. \begin{verbatim} % Declare program predicates pred cycle( vtx , vtx ). % Declare variables var vtx X, Y, Z. % Choose an ordering of nodes on the cycle. For each % vertex Y choose exactly one location X (the type vtx % is used to represent locations) 1 { cycle(X,Y): vtx(X) } 1. % Choose an ordering of nodes on the cycle, continued. % For each location X choose exactly one vertex Y 1 { cycle(X,Y): vtx(Y) } 1. % Enforce the hamiltonicity restriction X edge(Y,Z). cycle(n,Y), cycle(1,Z) -> edge(Y,Z). \end{verbatim} \paragraph*{Vertex-cover problem.} We specify the rule file only. The data file must define the vertex set of the graph (for instance, the statement {\tt vtx[1..n]}) will define the vertex set to be $\{1,\ldots, n\}$, where $n$ is a parameter entered from the command line). The data file must also list all the edges of the graph as facts $\mathit{edge}(a,b)$, where $\mathit{edge}$ is another data predicate. The main (and only) program predicate is $\mathit{incover}$. Atom $\mathit{incover}(X)$ represents the fact that the vertex $X$ is in a vertex cover. \noindent Rule file. \begin{verbatim} % Declare program predicates pred incover( vtx ) . % Declare variables var vtx X, Y. % Select a set of vertices for a vertex cover { incover(X) : vtx(X) } k. % Enforce the vertex-cover constraint: at least one end % of each edge must be in the cover edge(X,Y) -> incover(X) | incover(Y). \end{verbatim} \paragraph*{Schur numbers.} The data file specifies the range of integers to be partitioned, $n$, and the number of parts, $k$. This can be accomplished by two statements $\mathit{number}$ and $\mathit{part}$ are data predicates): ${\tt number[1..n].}$ and ${\tt part[1..k].}$ The main program predicate is $\mathit{inpart}$. Atom $\mathit{inpart}(X,P)$ represents the fact that number $X$ is included in part $P$. \noindent Rule file. \begin{verbatim} % Declare program predicates pred inpart(number,part). % Declare variables var number X,Y. var part P. % Assign each integer to exactly one part 1 { inpart(X,P) : part(P) } 1. % Enforce the sm-free constraint inpart(X,P), inpart(Y,P), inpart(X+Y,P) -> . \end{verbatim} \newpage \newcommand{\etalchar}[1]{$^{#1}$} %\begin{thebibliography}{ELM{\etalchar{+}}98} \begin{thebibliography}{AABdR00} \bibitem[AABdR00]{AABR2000} R.~Accorsi, C.~Areces, W.~Bouma, and M.~de~Rijke. \newblock Features as constraints. \newblock In {\em Proceedings of the Sixth Feature Interaction Workshop}, Glasgow, Scotland, May 2000. \bibitem[AAdR99]{AAR99} R.~Accorsi, C.~Areces, and M.~de~Rijke. \newblock Towards feature interaction via stable models. \newblock In {\em Proceedings of the Second Workshop on Formal Methods}, Florianópolis, Brasil, October 1999. \bibitem[ABS00]{Aura2000} T.~Aura, M.~Bishop, and D.~Sniegowski. \newblock Analyzing single-server network inhibition. \newblock In {\em Proceedings of the IEEE Computer Security Foundations Workshop}, pages 108--117, Cambridge, UK, July 2000. IEEE Computer Society Press. \bibitem[AM00]{AM2000} L.C. Aiello and F.~Massacci. \newblock An executable specification language for planning attacks to security protocols. \newblock In {\em Proceedings of the IEEE Computer Security Foundations Workshop}, pages 88 --102, Cambridge, UK, July 2000. IEEE Computer Society Press. \bibitem[BBG{\etalchar{+}}01]{BBGBW2001:padl} M.~Balduccini, M.~Barry, M.~Gelfond, M.~Nogueira, and R.~Watson. \newblock An a-prolog decision support system for the space shuttle. \newblock In {\em Proceedings of the Third International Symposium on Practical Aspects of Declarative Languages}, Las Vegas, Nevada, 2001. Springer-Verlag. \bibitem[BF91]{bf91a} N.~Bidoit and C.~Froidevaux. \newblock Negation by default and unstratifiable logic programs. \newblock {\em Theoretical Computer Science}, 78(1, (Part B)):85--112, 1991. \bibitem[DNK97]{DNK97} Y.~Dimopoulos, B.~Nebel, and J.~Koehler. \newblock Encoding planning problems in non-monotonic logic programs. \newblock In {\em Proceedings of the Fourth European Conference on Planning}, pages 169--181, Toulouse, France, September 1997. Springer-Verlag. \bibitem[ET00]{et00a} D.~East and M.~Truszczy\'{n}ski. \newblock Datalog with constraints. \newblock In {\em Proccedings of the Seventeenth National Conference on Artificial Intelligence (AAAI-2000)}, pages 163--168, 2000. \bibitem[ET01]{et01a} D.~East and M.~Truszczy{\'n}ski. \newblock Answer-set programming with propositional schemata. \newblock Submitted, 2001. \bibitem[ET01]{ET2001:asp} D.~East and M.~Truszczy\'{n}ski. \newblock More on wire routing with asp. \newblock In {\em Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning}, pages 39--44, Stanford, USA, March 2001. AAAI Press. \bibitem[ELM{\etalchar{+}}97]{elmps97} T.~Eiter, N.~Leone, C.~Mateis, G.~Pfeifer, and F.~Scarcello. \newblock A deductive system for non-monotonic reasoning. \newblock In {\em Logic programming and nonmonotonic reasoning (Dagstuhl, Germany, 1997)}, volume 1265 of {\em {L}ecture {N}otes in {C}omputer {S}cience}, pages 364--375. Springer, 1997. \bibitem[ELM{\etalchar{+}}98]{elmps98} T.~Eiter, N.~Leone, C.~Mateis, G.~Pfeifer, and F.~Scarcello. \newblock A {KR} system {\tt dlv}: Progress report, comparisons and benchmarks. \newblock In {\em Proceeding of the Sixth International Conference on Knowledge Representation and Reasoning (KR '98)}, pages 406--417. Morgan Kaufmann, 1998. \bibitem[ELW00]{ELW2000:cl} E.~Erdem, V.~Lifschitz, and M.D.F. Wong. \newblock Wire routing and satisfiability planning. \newblock In {\em Proceedings of the First International Conference on Computational Logic, Automated Deduction: Putting Theory into Practice}, pages 822--836, London, U.K., July 2000. Springer-Verlag. \bibitem[EH01]{EspHel:SPIN2001} J.~Esparza and K.~Heljanko. \newblock Implementing {LTL} model checking with net unfoldings. \newblock In {\em Proceedings of the 8th International {SPIN} Workshop on Model Checking of Software ({SPIN}'2001)}, Toronto, Canada, May 2001. \newblock Accepted for publication. \bibitem[GG01]{GG2001:asp} M.~Gelfond and J.~Galloway. \newblock Diagnosing dynamic systems in {A­Prolog}. \newblock In {\em Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning}, pages 160--166, Stanford, USA, March 2001. AAAI Press. \bibitem[GL88]{gl88} M.~Gelfond and V.~Lifschitz. \newblock The stable semantics for logic programs. \newblock In R.~Kowalski and K.~Bowen, editors, {\em Proceedings of the 5th {I}nternational {C}onference on {L}ogic {P}rogramming}, pages 1070--1080. MIT Press, 1988. \bibitem[Hel99a]{Heljanko99:csp} K.~Heljanko. \newblock Minimizing finite complete prefixes. \newblock In H.-D. Burkhard, L.~Czaja, H.S. Nguyen, and P.H. Starke, editors, {\em Concurrency, Specification and Programming (Proceedings of the CS\&P'99 Workshop)}, pages 83--95, Warsaw, Poland, 1999. \bibitem[Hel99b]{Heljanko:Fundamenta99} K.~Heljanko. \newblock Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe {Petri} nets. \newblock {\em Fundamenta Informaticae}, 37(3):247--268, 1999. \bibitem[HMN00]{HMN2000:nmr} M.~Hietalahti, F.~Massacci, and I.~Niemel\"a. \newblock {DES}: a challenge problem for nonmonotonic reasoning systems. \newblock In {\em Proceedings of the 8th International Workshop on Non-Monotonic Reasoning (cs.AI/0003073)}, Breckenridge, Colorado, USA, April 2000. \newblock cs.AI/0003039. \bibitem[HN01a]{HN2001:asp} K.~Heljanko and I.~Niemel\"a. \newblock Answer set programming and bounded model checking. \newblock In {\em Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning}, pages 90--96, Stanford, USA, March 2001. AAAI Press. \bibitem[HN01b]{HN2001:lpnmr} K.~Heljanko and I.~Niemel\"a. \newblock Bounded {LTL} model checking with stable models. \newblock In {\em Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning}, Vienna, Austria, September 2001. Springer-Verlag. \bibitem[JNSY00]{JNSY2000:kr} T.~Janhunen, I.~Niemel\"a, P.~Simons, and J.~You. \newblock Unfolding partiality and disjunctions in stable model semantics. \newblock In A.G. Cohn, F.~Guinchiglia, and B.~Selman, editors, {\em Proceedings of the Seventh International Conference on Principles of Knowledge Representation and Reasoning}, pages 411--419, Breckenridge, Colorado, USA, April 2000. Morgan Kaufmann Publishers. \bibitem[Kor00]{korf00} Richard~E. Korf. \newblock Recent progress in the design and analysis of admissible heuristic functions. \newblock In {\em Proccedings of the Seventeenth National Conference on Artificial Intelligence (AAAI-2000)}, pages 1165--1170, 2000. \bibitem[Kow74]{ko74} R.~Kowalski. \newblock Predicate logic as a programming language. \newblock In {\em Proceedings of IFIP 74}, pages 569--574, Amsterdam, 1974. North Holland. \bibitem[Kow79]{ko79} R.~Kowalski. \newblock {\em Logic for Problem Solving}. \newblock North Holland, Amsterdam, 1979. \bibitem[Lif99]{li99b} V.~Lifschitz. \newblock Answer set planning. \newblock In {\em Logic programming, Proceedings of the 1999 International Conference on Logic Programming}, pages 23--37. MIT Press, 1999. \bibitem[Lif00]{lif00} V.~Lifschitz. \newblock Missionaries and cannibals in the causal calculator. \newblock In {\em Principles of Knowledge Representation and Reasoning, Proceedings of the Seventh International Conference (KR2000)}, pages 85 -- 96. Morgan Kaufmann Publishers, 2000. \bibitem[LRS98]{LRS98:tacas} X.~Liu, C.R. Ramakrishnan, and S.A. Smolka. \newblock Fully local and efficient evaluation of alternating fixed points. \newblock In Bernhard Steffen, editor, {\em Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, pages 5--19, Lisbon, Portugal, March/April 1998. Springer-Verlag. \bibitem[McC80]{mca80} J.~McCarthy. \newblock Circumscription --- a form of non-monotonic reasoning. \newblock {\em Artificial Intelligence}, 13(1-2):27--39, 1980. \bibitem[McD82]{mcd82} D.~McDermott. \newblock Nonmonotonic logic {II}: nonmonotonic modal theories. \newblock {\em Journal of the ACM}, 29(1):33--57, 1982. \bibitem[MD80]{mcdd80} D.~McDermott and J.~Doyle. \newblock Nonmonotonic logic {I}. \newblock {\em Artificial Intelligence}, 13(1-2):41--72, 1980. \bibitem[Moo85]{mo85} R.C. Moore. \newblock Semantical considerations on nonmonotonic logic. \newblock {\em Artificial Intelligence}, 25(1):75--94, 1985. \bibitem[MT89]{mt89c} W.~Marek and M.~Truszczy\'{n}ski. \newblock Stable semantics for logic programs and default theories. \newblock In E.Lusk and R.~Overbeek, editors, {\em Proceedings of the North American Conference on Logic Programming}, pages 243--256. MIT Press, 1989. \bibitem[MT99]{mt99} V.W. Marek and M.~Truszczy\'{n}ski. \newblock Stable models and an alternative logic programming paradigm. \newblock In K.R. Apt, W.~Marek, M.~Truszczy\'{n}ski, and D.S. Warren, editors, {\em The Logic Programming Paradigm: a 25-Year Perspective}, pages 375--398. Springer Verlag, 1999. \bibitem[Nie99]{nie99} I.~Niemel\"{a}. \newblock Logic programming with stable model semantics as a constraint programming paradigm. \newblock {\em Annals of Mathematics and Artificial Intelligence}, 25(3-4):241--273, 1999. \bibitem[NS96]{ns96} I.~Niemel{\"a} and P.~Simons. \newblock Efficient implementation of the well-founded and stable model semantics. \newblock In {\em {Proceedings of JICSLP-96}}. MIT Press, 1996. \bibitem[NS00]{ns00} I.~Niemel{\"a} and P.~Simons. \newblock Extending the Smodels system with cardinality and weight constraints. \newblock In J.~Minker, editor, {\em Logic-Based Artificial Intelligence}, pages 491--521. Kluwer Academic Publishers, 2000. \bibitem[Par01]{Parmar2001:asp} A.~Parmar. \newblock A declarative implementation of planning with control. \newblock In {\em Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning}, pages 160--166, Stanford, USA, March 2001. AAAI Press. \bibitem[Rei78]{re78} R.~Reiter. \newblock On closed world data bases. \newblock In H.~Gallaire and J.~Minker, editors, {\em Logic and data bases}, pages 55--76. Plenum Press, 1978. \bibitem[Rei80]{re80} R.~Reiter. \newblock A logic for default reasoning. \newblock {\em Artificial Intelligence}, 13(1-2):81--132, 1980. \bibitem[SBM01]{SBM2001:asp} T.C. Son, C.~Baral, and S.~McIlraith. \newblock Extending answer set planning with sequence, conditional, loop, non-deterministic choice, and procedure constructs. \newblock In {\em Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning}, pages 202--209, Stanford, USA, March 2001. AAAI Press. \bibitem[SGN99]{SGN99:cp} T.~Soininen, E.~Gelle, and I.~Niemel\"a. \newblock A fixpoint definition of dynamic constraint satisfaction. \newblock In Joxan Jaffar, editor, {\em Proceedings of the Fifth International Conference on Principles and Practice of Constraint Programming}, pages 419--433, Alexandria, Virginia, USA, October 1999. Springer-Verlag. \bibitem[Sim00]{Simons2000:phd} P.~Simons. \newblock Extending and implementing the stable model semantics. \newblock Doctoral Dissertation. Research report A58, Helsinki University of Technology, Helsinki, Finland, April 2000. \bibitem[SL01]{SL2001:asp} T.C. Son and J.~Lobo. \newblock Reasoning about policies using logic programs. \newblock In {\em Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning}, pages 210--216, Stanford, USA, March 2001. AAAI Press. \bibitem[SN99]{SN99:padl} T.~Soininen and I.~Niemel\"a. \newblock Developing a declarative rule language for applications in product configuration. \newblock In Gopal Gupta, editor, {\em Proceedings of the First International Workshop on Practical Aspects of Declarative Languages}, pages 305--319, San Antonio, Texas, January 1999. Springer-Verlag. \bibitem[SNTS00]{SNTS2000:ecai} T.~Soininen, I.~Niemel\"a, J.~Tiihonen, and R.~Sulonen. \newblock Unified configuration knowledge representation using weight constraint rules. \newblock In {\em Workshop Notes of the ECAI'2000 Configuration Workshop}, pages 79--84, Berlin, Germany, August 2000. \bibitem[SNTS01]{SNTS2001:asp} T.~Soininen, I.~Niemel\"a, J.~Tiihonen, and R.~Sulonen. \newblock Representing configuration knowledge with weight constraint rules. \newblock In {\em Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning}, pages 195--201, Stanford, USA, March 2001. AAAI Press. \bibitem[Syr99]{Syrjanen99:dtyo} T.~Syrj\"anen. \newblock A rule-based formal model for software configuration. \newblock Research Report A55, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Helsinki, Finland, December 1999. \bibitem[Syr00a]{Syrjanen2000:cl} T.~Syrj\"anen. \newblock Including diagnostic information in configuration models. \newblock In {\em Proceedings of the First International Conference on Computational Logic, Automated Deduction: Putting Theory into Practice}, pages 837--851, London, U.K., July 2000. Springer-Verlag. \bibitem[Syr00b]{Syrjanen2000:ecai} T.~Syrj\"anen. \newblock Optimizing configurations. \newblock In {\em Workshop Notes of the ECAI'2000 Configuration Workshop}, pages 85--90, Berlin, Germany, August 2000. \bibitem[TB01]{TB2001:asp} L.~Tuan and C.~Baral. \newblock Effect of knowledge representation on model based planning: Experiments using logic programming encodings. \newblock In {\em Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning}, pages 110--115, Stanford, USA, March 2001. AAAI Press. \bibitem[VRS91]{vrs91} A.~{Van Gelder}, K.A. Ross, and J.S. Schlipf. \newblock The well-founded semantics for general logic programs. \newblock {\em {Journal of the ACM}}, 38(3):620--650, 1991. \bibitem[Var00]{Varpaaniemi2000:fi} K.~Varpaaniemi. \newblock Stable models for stubborn sets. \newblock {\em Fundamenta Informaticae}, 43(1--4):355--375, 2000. \end{thebibliography} %\newpage %\bibliography{ini,smodels} %\bibliographystyle{alpha} \newpage \section{Slides} \label{slides} \end{document}