Esra Erdem talked about her paper "Wire routing and satisfiability planning," joint with Vladimir Lifschitz and Martin Wong. Wire routing is the problem of determining the physical locations of all the wires interconnecting the circuit components on a chip. Since the wires cannot intersect with each other, they are competing for limited spaces, thus making routing a difficult combinatorial optimization problem. We present a new approach to wire routing that uses action languages and satisfiability planning. Its idea is to think of each path as the trajectory of a robot, and to understand a routing problem as the problem of planning the actions of several robots whose paths are required to be disjoint. The new method differs from the algorithms implemented in the existing routing systems in that it always correctly determines whether a given problem is solvable, and it produces a solution whenever one exists.
Joohyung Lee talked about his work on formalizing the Zoo World proposed by Erik Sandewall. This is joint work with Hudson Turner. This domain contains the main ingredients of a classical zoo: cages, animals in the cages, gates between two cages as well as gates between a cage and the exterior. There are animals of several species, including humans. Actions in the world may include movement within and between cages, opening and closing gates, feeding the animals, one animal killing and eating another, riding animals, etc.
Vladimir Lifschitz led the discussion of Selim Erdogan's formalization of the Traffic World proposed by Erik Sandewall. In this world, there are vehicles moving continuously with well defined velocities along roads with well defined lengths, respecting speed limits and other restrictions on the vehicle's behaviors.
Vladimir Lifschitz talked about the semantics of negation as failure in connection with the additional features available in Version 2 of smodels. The meaning of "choice rules" such as
{p,q} :- ...
can be explained by reducing them to logic programs with nested expressions. For instance, the head of the rule above can be thought of as shorthand for
((p ; not p) , (q not q)).
A dry run of Esra Erdem's forthcoming talk at the 8th International Workshop on Nonmonotonic Reasoning, "Fages' theorem and answer set programming," joint with Yuliya Babovich and Vladimir Lifschitz. The paper generalizes a theorem by Francois Fages that describes the relationship between the completion semantics and the answer set semantics for logic programs with negation as failure. The study of this relationship is important in connection with the emergence of answer set programming. Whenever the two semantics are equivalent, answer sets can be computed by a satisfiability solver, and the use of an answer set solver such as smodels and dlv is unnecessary. A logic programming representation of the blocks world due to Ilkka Niemelae is discussed as an example.
Vladimir Lifschitz talked about the "logic of here-and-there." This is a 3-valued (monotonic propositional) logic invented 70 years ago by Arend Heyting. David Pearce showed how this logic can be used to prove the "monotonic" (or "strong") equivalence of logic programs. (We say that a program A is monotonically equivalent to a program A' if, for every logic program B, the result of appending B to A has the same answer sets as the result of appending B to A'.) If two programs are monotonically equivalent then they have the same answer sets (take B to be empty), but not the other way around. The study of monotonic equivalence is important, because we learn from it how parts of a logic program can be simplified without looking at the rest of the program.
Monica Nogueira from UT El Paso visited Austin to tell us about her paper "A-Prolog as a tool for declarative programming," joint with Marcello Balduccini and Michael Gelfond, and to demonstrate the system described in the paper. In this work, smodels is used to characterize the dynamic behavior of combinatorial circuits with delays. The paper will be presented at the 12th International Conference on Software Engineering and Knowledge Engineering this summer.
Esra Erdem reviewed the paper "Formulating diagnostic problem solving using an action language with narratives and sensing" by Chitta Baral, Sheila McIlraith and Tran Cao Son, published in the Proceedings of KR-2000. She showed how one of the problems described in the paper can be formalized and solved using the Causal Calculator. Replacing the language L used in the paper by the language of the Causal Calculator allows us to simplify the representation of the problem somewhat by eliminating the need for "wildcard actions," such as break(x). Instead of postulating
break(x) causes ab(x)
we can express that fluent ab(x) can change its value from false to true by writing
caused ab(x) if ab(x) after -ab(x).
loc(block) :: inertialFluent(location).
A regular fluent is a fluent with numerical values such that the effect of several concurrently executed actions on it can be computed by adding the effects of the individual actions. The need to study this class of fluents is related to some of the difficultues uncovered in Vladimir Lifschitz's work on elaboration tolerance (Missionaries and cannibals in the Causal Calculator).