The Causal Calculator: A Glimpse of Version 2.0
Our Goals
Here are some of the goals that we'll strive to achieve in Version 2.0.
- We'll implement the causal logic with multi-valued constants described
in the paper
Causal
laws and multi-valued fluents by Giunchiglia, Lee, Lifschitz and
Turner, which extends the original system of causal logic by McCain and
Turner in the same way in which C+ extends C. The representations of graph
problems below illustrate how this can be useful.
- We'll distinguish between declarations of objects and declarations of
constants. The word "constant" will be understood as in new causal logic
and in action language C+. Declarations of objects serve to
specify the extents of sorts, which, in turn, are used to specify the
domains of constants and the ranges of variables. See, for instance,
files bw-serializable,
bw-serializable-test, and
color.
- "Rigid" fluents -- fluents that never actually change their values
-- will be implemented as constants in the sense of causal logic; see,
for instance, files bw-sizes and
bw-sizes-test.
- We'll allow a 'where' clause, containing a test, at the end of a rule,
as, for instance, at the end of file
bw-serializable. This
will make grounding more efficient.
- Arithmetical expressions in rules will be automatically evaluated, so
that formulas like "I is J+1" will not be needed. See, for instance,
the definition of 'edge' in file
graph-description.
- The input language will not depend so heavily on Prolog. Prolog code
will be used for only one purpose -- for describing user-defined tests;
these definitions will be placed in separate files. See
the new syntax of tests.
- Symbol =, corresponding to 'eq' in the current version, will be used
in a more symmetric way: values and constants will be allowed in both sides.
See, for instance, bw-serializable.
- Statically determined fluents will be implemented. This is a recent
addition to C+, and it is not yet documented. Such fluents are not
allowed in the heads of dynamic propositions; on the other hand, the
static propositions containing such a fluent in the head will completely
determine its possible values. Statically determined fluents are used, for
instance, in file bw-perfect. Rigid fluents
are a special case of statically determined fluents.
Queries about Transition Diagrams
In the new version of CCalc, the language of queries will become more
expressive. A query about a transition diagram will consist of two
components. One is an integer, called maxstep, that specifies the length
of the paths the query is about. It is similar to maxtime in the current
version, and its value determines how to turn the given action description
into a causal theory.
The second component of a query is a causal theory whose models are the
paths that we are interested in. Given a query, CCalc will look for a path
in the transition diagram that is a model of the query, that is to say, for
a common model of two causal theories -- one obtained by translating the
action description, the other representing the query.
The plan directive in the current version of CCalc corresponds to the
queries in which all constants are exogenous. This special case will be
now represented by the symbol anyHistory, defined in file
macros.std and used, for instance, in the
second query in bw-serializable-test.
Another kind of queries allows the values of fluents to be arbitrary
and postulates the closed world assumption for Boolean action constants, as,
for instance, in the first query in that file.
Modes of Operation
The new CCalc, like the current version, will be able to operate in
basic mode, transition mode, and history mode. But syntactically the modes
will differ from each other in a different way: the mode will be determined
by how the symbol maxstep is treated in the input file.
In basic mode the value of maxstep is not specified, as in our examples
of graph problems. The C+ propositions in the input file (if any) will be
translated into causal rules using the default value maxstep=0. Typically,
in this case the input file will contain no dynamic propositions, and in the
process of operation of CCalc the sat command will be used to find a model
of the given causal theory.
In transition mode maxstep is specified in a query, as in
bw-serializable-test.
CCalc will look for the paths satisfying the query, as discussed above.
In history mode the value of maxstep is specified globally, by a macro.
After this macro, file history.std will be
usually included. See, for instance,
bw-serializable-h-test.
When history mode is used to do what can be accomplished in transition mode
as well, as in the example above, the set of clauses produced by CCalc will
be essentially the same in both modes (which is not quite the case in the
current version). In such situations, the computation will be done more
efficiently in transition mode, because of the use of shifting. Another
advantage of transition mode is that it allows the user to provide a range
of values for maxstep instead of a single value, and to include queries
with different values of maxstep in the same input file. On the other hand,
history mode is more flexible than transition mode because it allows the
user to refer to specific time instants in the description of the domain.
Examples of Input Files for Version 2.0
The first group of files shows how to describe a graph and to encode two
search problems -- graph coloring and finding a clique of a given size
-- using causal logic with multi-valued constants.
To find a coloring or a clique, we'll use the loadf command to load the
corresponding input file, and then the sat command to find an interpretation
satisfying the set of clauses generated after the first step:
| ?- loadf('color').
% ...
yes
| ?- sat.
The next example is a description of the blocks world in C+ similar
to the one given in the paper
Additive
fluents by Lee and Lifschitz. The first test file illustrates
running CCalc in transition mode and contains
two queries: a temporal projection problem and a planning problem. The
second test file reformulates one of these queries in history mode.
We'll submit these queries using the query command:
| ?- loadf('bw-serializable-test').
% ...
yes
| ?- query 1.
We can enhance that description of the blocks world by classifying
blocks into large and small -- a distinction that doesn't depend on the state.
The descriptions of the blocks world above allow physically impossible
states -- those in which some blocks form circular configurations in space.
For this reason, they may be inadequate unless combined with an explicit
description of a specific, physically possible, initial state. The method
proposed in the paper
Transitive
closure, answer sets and predicate completion by Erdem and Lifschitz
allows us to remove this restriction.
Standard Files
Two files will be automatically included at the beginning of
every CCalc input file:
To run CCalc in history mode, the user will include the file that translates
from C+ into causal logic:
CCalc home page