Logic-based subsumption architecture.
We describe a logic-based AI architecture based on Brooks' subsumption architecture. In this architecture, we axiomatize different layers of control in First-Order Logic (FOL) and use independent theorem provers to derive each layer's outputs given its inputs. We implement the subsumption of lower layers by higher layers using nonmonotonic reasoning principles. In particular, we use circumscription to make default assumptions in lower layers, and nonmonotonically retract those assumptions when higher layers draw new conclusions. We also give formal semantics to our approach. Finally, we describe layers designed for the task of robot control and a system that we have implemented that uses this architecture for the control of a Nomad 200 mobile robot.Our system combines the virtues of using the represent-and-reason paradigm and the behavioral-decomposition paradigm. It allows multiple goals to be serviced simultaneously and reactively. It also allows high-level tasks and is tolerant to different changes and elaborations of its knowledge in runtime. Finally, it allows us to give more commonsense knowledge to robots. We report on several experiments that empirically show the feasibility of using fully expressive FOL theorem provers for robot control with our architecture and the benefits claimed above.
Introduction
In (Brooks 1986), Rodney Brooks provided a decomposition
of the problem of robot control into layers corresponding
to levels of behavior, rather than according to
a sequential, functional form. Within this setting, he
introduced the idea of subsumption, that is, that more
complex layers could not only depend on lower, more
reactive layers, but could also influence their behavior.
The resulting architecture was one that could service
simultaneously multiple, potentially conflicting goals in
a reactive fashion, giving precedence to high priority
goals.
Because of its realization in hardware, the architecture
lacks declarativeness, making it difficult to implement
higher-level reasoning and making its semantics
unclear. Furthermore, the increasing hardware complexity
with new layers introduces scaling problems. Fi-
nally, relying on hardware specifications, the architecture
is specifically oriented towards robot control and
is not applicable to software agents or other software-based
intelligent agents. The problem of extending similar
architectures to more complex tasks and goals and
to agents that are not necessarily physical, has already
been raised and discussed in general lines by (Minsky
1985) and (Stein 1997), but, to our knowledge, no practical
AI architecture has been developed along these
lines.
In this paper we describe an architecture modeled
in the spirit of Brooks' Subsumption Architecture but
which relies on a logical framework and which has
wider applicability and extendability in the manner described
above. Our Logic-Based Subsumption Architecture
includes a set of logical theories, each
corresponding to a layer in the sense of Brooks' archi-
tecture. Each layer is supplied with a separate theorem
prover, allowing the system of layers to operate concur-
rently. We use an approximation of nonmonotonic reasoning
to model the connections between the theories.
By allowing the layers to make nonmonotonic assump-
tions, each layer's performance is independent of the
performance of other layers, thus supporting reactiv-
ity. We demonstrate our architecture modeling Brooks'
first two layers, showing empirically that the layer in
greatest demand of reactivity is sufficiently fast (0.2-
0.3 seconds per control-loop cycle). This empirical result
shows that general-purpose theorem provers can be
used in intelligent agents without sacrificing reactivity.
The remainder of the paper is organized as follows:
After giving a brief introduction to Brooks' system and
logical AI, we describe a general architecture that embodies
a collection of theories and uses their decoupling
and interactions to exhibit complex behaviors. Then,
we describe our representation for the first two layers of
Brooks' system and describe how subsumption and the
general operation of the system can be implemented using
theorem proving and negation-as-failure techniques.
We give formal semantics to our approach using circum-
scription, discuss implementation issues and conclude
with comparisons to related work and a sketch of future
directions.
This work is a first step towards creating a general
logic-based AI architecture that is efficient, scalable and
supports reactivity, an architecture that is our long-term
goal.
Background
2.1 Brooks' Subsumption Architecture
Brooks showed that decomposing a system into parallel
tasks or behaviors of increasing levels of competence, as
opposed to the standard functional decomposition, can
be advantageous. Whereas a typical functional decomposition
might resemble the sequence:
sensors
task recognition ! motor control,
Brooks would decompose the same domain as follows:
avoid objects
monitor changes ! identify objects ! plan actions
reason about object behavior
increasing levels of competence. Potential
benefits from this approach include increased
robustness, concurrency support, incremental construc-
tion, and ease of testing.
An underlying assumption is that complex behavior
is a product of a simple mechanism interacting with a
complex environment. This focus on simplicity led to a
design where each individual layer is composed of simple
state machine modules operating asynchronously
without any central control.
In general, the different layers are not completely in-
dependent. For example, in the decomposition above,
wandering and exploring depend on the robot's ability
to avoid objects. Often, the system may be able to service
these multiple goals in parallel, despite the depen-
dence. However, occasionally, the goals of one layer will
conflict with those of another layer. In such instances
we would expect higher priority goals to override lower
priority ones. To address this issue, the Subsumption
Architecture provides mechanisms by which higher layers
may interfere with the operation of lower layers.
First, it is possible for higher layers to observe the state
of lower layers. Second, it is possible for higher layers
to inhibit outputs and/or suppress (that is, override)
inputs to modules in a lower layer. Consequently, more
competent layers can adjust the behavior of more reactive
layers. At the same time, it is possible to have high
priority tasks in a lower layer (such as halting when an
object is dead-ahead) continue to have high precedence
by simply not allowing any higher layers to tamper with
those particular tasks.
In (Brooks 1986), Brooks describes in detail the first
three layers of one particular robot control system he
implemented using the Subsumption Architecture con-
cept. The first two are shown in Figure 1. We briefly
describe the three layers here:
Avoid The most basic layer in the system endows the
robot with obstacle avoidance capabilities. When an
obstacle appears directly ahead in the robot's path,
it halts before colliding. In general, whenever there
are obstacles in its vicinity, it uses their direction and
distance with respect to the robot to compute a new
heading which moves it away from the obstacles as
much as possible.
In more detail, the layer accepts sonar readings of
the robot's surroundings into its sonar module which
outputs a map of the vicinity based on these read-
ings. The collide module checks if there is an obstacle
directly ahead and, if there is, forces the robot
to stop regardless of what other modules are doing.
The feelforce module uses the map to calculate a
combined repulsive "force" that the surrounding objects
exert on the robot. The runaway module checks
if this force is significant enough to pay attention to
and, in the case that it is, determines the new heading
and speed for the robot to move away from the force.
The turn module commands the robot to make the
required turn, then passes the speed on to the forward
module which, if not in a halt state, commands the
robot to move forward with the specified speed. The
further away the robot gets, the smaller the speed
computed by the runaway module.
Wander The wander layer consists of two modules
which, together with the avoid layer, cause the robot
to move around aimlessly when it is not otherwise oc-
cupied. Every so often, the wander module chooses a
new random direction for the robot to move in. The
avoid module combines it with the output of the
avoid layer's feelforce module, computing an over-all
heading that suppresses the input to the avoid
layer's turn module. Hence, when wander mode is
active, it overrides the default heading computed by
the avoid layer.
Explore This layer begins to add some primitive goal-directed
behavior to the robot's repertoire. The robot
periodically checks to see if it is idle and, if so, chooses
some location in the distance to head towards and
explore. While in exploration mode, it inhibits the
wander layer so that it remains more or less on track
towards its destination. However, like the wander
layer, it takes advantage of the avoid layer's capabilities
to prevent collisions. As we don't model this
layer in this paper (the first two layers are sufficient
to demonstrate our proposal), we refer the reader to
(Brooks 1986) for details.
2.2 Logic & Circumscription
Since the early days of AI, logic held a promise to serve
as a main knowledge representation language in the future
intelligent machine (McCarthy 1958). In the last
decade, theorem provers became wide spread as formal
verification tools and lately a few robot systems
wielding logic have emerged (e.g., (Shanahan 1996),(Gi-
acomo, Lesperance, & Levesque 1997)).
In the logical paradigm, McCarthy's Circumscription
(McCarthy 1980) is one of the first major nonmonotonic
reasoning tools. Since its debut, the nonmonotonic reasoning
line of work has expanded and several textbooks
now exist that give a fair view of nonmonotonic reasoning
and its uses (e.g., (Brewka 1991), (Antoniou
1997), (Brewka, Dix, & Konolige 1997), (D.M. Gabbay
1994), (Sandewall 1994), (Shanahan 1997)). The motivations
for nonmonotonic reasoning vary from formalizing
Common Sense reasoning through Elaboration Tolerance
and representing uncertainty to Belief Revision.
We do not expand on these motivations here; the reader
may look at (Shanahan 1997),(McCarthy 1998),(Pearl
1990) and (Antoniou 1997) for further details in these
directions.
McCarthy's Circumscription formula (McCarthy
feelforce runaway turn
forward
avoid
wander
collide
sonar
heading
turn
fwd
Object
wander_heading
encoders
sensor_readings
robot
heading
force
robot
robot
speed

Figure

1: Layers 0 and 1 of Brooks' Subsumption Architecture robot control system.
says that in the theory A, with parameter relations and
function sequences is a minimal element such
that A(P; Z) is still consistent, when we are allowed to
vary Z in order to allow P to become smaller.
Take for example the following simple theory:
Then, the circumscription of block in T , varying noth-
ing, is Circ[T
block)] which is equivalent to
By minimizing block we concluded that there are no
other blocks in the world other than those mentioned
in the original theory T .
3 Logic-Based Subsumption
Architecture
This section is dedicated to describing the proposed ar-
chitecture. We first give an intuitive account and an
approximation of the semantics of the system. Then
we describe the architecture in more detail and give the
ideas and goals embodied in it. Finally we describe how
to build a system that approximates that of Brooks' in
the proposed way.
3.1 Intuition
The Logic-Based Subsumption Architecture (LSA) is
composed of a sequence of logical theories, each supplied
with its own theorem prover. Each of the theories
communicates with some of those "underneath" it in
the sequence (those that are "subsumed"), modifying
and controlling the behavior of these "lower-level" the-
ories. Aside from this collection of theories there are
sensors that affect the theories and manipulators that
are affected by the theories (more precisely, by the results
found by the theorem provers). In the description
that follows we assume that the architecture is used to
control a cylindrical robot that has sonar sensors on its
perimeter and wheels that control its motion. No other
sensors or manipulators are assumed (at this stage).
We want a system based on these premises to work in
a loop as follows: First, the physical sonars collect their
data and assert it in the form of logical axioms, such as
sonar reading(sonar dist. These axioms
are added 1 to the appropriate theory in the sequence
of theories comprising the system. At the same time,
we assert any input coming to each layer from a higher-level
theory (both kinds of input are replaced each cycle
with the new inputs). Then, we ask the theorem prover
of each layer to find the required outputs for that layer,
having some of the outputs specify actions for the ma-
nipulators. After reaching the conclusions, we transmit
the relevant ones (those outputs that specify actions for
the manipulators) to the robot manipulators and, while
the robot executes the requested actions, the loop starts
again.

Figure

2 illustrates this process.
Theory 1
Theory 0
Sensors Effectors

Figure

2: An abstract diagram of the LSA.
1 At each iteration of sonar readings, we replace the previous
inputs with the new ones.
The Logic-Based Subsumption Architecture should
follow this general pattern, making sure that the loop is
fast enough so that at the time we get to our conclusions
the world is not too different from the world we based
these conclusions on (e.g., making sure that the robot
does not fall off the cliff while planning a way to avoid
the cliff edge). Notice that, in fact there are several
loops with different times (for the different layers and
theorem provers) and the reactive loop is the one that
counts for the speed of the overall loop. We describe
how this behavior is achieved in the next section.
3.2 The architecture
Behavioral decomposition The first important
idea we borrow from Brooks' architecture is that of
decomposing the domain along behavioral lines rather
than along the standard sequential functional lines.
This change in paradigm makes it possible to view the
robot control problem as a set of loosely coupled processes
and, hence, parallelizable. We claim that we
get similar performance benefits when applying this
paradigm to a logical version of the Subsumption Architecture

To build the LSA, we represent each layer with an axiomatization
of the layer's behavior, that is, the layer's
input, output and state, including any dependencies
between these that support the task of this layer (in
our architecture, these layer-inputs and layer-outputs
are predicates/functions that are intended to go either
from/to sensors/actuators or from/to lower layers).
Ignoring inter-layer interactions for a moment, the
output of each layer is determined by running a separate
theorem prover for that layer only. These treatment
and representation buy us a few benefits. First,
because the axiomatization of a layer is generally much
smaller than that of the whole system, each cycle will be
less computationally expensive than running one theorem
prover over the whole compound axiomatization.
Second, by decoupling the different layers of behavior
in this way, it becomes possible to achieve more reactive
behavior. As in Brooks' system, lower layers controlling
basic behaviors do not need to wait on higher layers
to have completed their computations before they can
respond to situations. Rather, since lower layers are
trusted to be autonomous (if the higher layer is not ac-
tive, the lower layer will still behave validly) and those
layers will have simpler axiomatizations in general, the
cycle time to compute their outputs can be shorter than
that of higher, more complex layers, leading to an over-all
high performance. This is important if, for example,
we want the robot to continue avoiding obstacles as it
tries to plan its next line of action.
Note that, although the module is an important construct
in Brooks' architecture, in our representation
modules serve mostly as "syntactic sugar." They provide
conceptual clarity with regard to the operation of
a layer a given theory denotes. We hasten to point
out, however, that the relative independence between
module axiomatizations could also be exploited, e.g., to
have a separate theorem proving session to determine
the intermediate module outputs, making it possible to
pipeline the operation of a layer.
Subsumption Principles Of course, the layers are
not fully independent. A fundamental feature of
Brooks' Subsumption Architecture is the ability of
higher layers to observe and interfere with the operation
of the lower layers. In particular, the suppression
and inhibition capabilities provide a means by which
the otherwise independent layers may interact, allowing
high-level goals to override/adjust default low-level re-active
behavior. We adopt the view that, together with
the task-based decomposition idea, this coupling approach
represents an important and natural paradigm
for an intelligent agent in general and robot control in
particular (see (Stein 1997)).
However, implementing this idea in a logical setting
raises the following issue: In general, when one layer
overrides another, the two disagree on what some particular
module input should be. Therefore, the two
corresponding theories will be inconsistent. We need
to formalize the higher-layer theory's precedence over
the lower-layer's in such a way that (a) if there is no
conflict, all the facts in either theory hold in the overall
state of the system, (b) in the event of a conflict, the
overall state sides with the higher layer, and (c) independent
facts (e.g., the inputs to either layer) remain
unchanged.
A number of techniques developed in the logic com-
munity, such as nonmonotonic techniques and belief re-
vision, are applicable. We have chosen to use circum-
scription, although we agree that other approaches may
be equally interesting and appropriate.
Circumscription-based Subsumption As described
earlier, each layer is a logical theory. We
distinguish three parts of the logical theory: (1) the
Body of the level, (2) the Sensory Latch and the Input
Latch and (3) the Output (see figure 3). The Body of
the layer is the constant theory for that layer. The
Latches are used to accept the input and replace it
every cycle (rather than accumulate it). The Output
is simply the output sentences proved by our layer
(including the latches).
In the following, assume an arbitrary level i and that
the theory in that layer is in a language L. We distinguish
the "input language" L I ae L, which constitutes
the language that is allowed in the Latches of that layer.
This is the language by which the theory is influenced
and it serves for the assertions coming from the sensors
and higher-level layers. The "output language"
ae L is used to limit the queries that the theory
can be asked. This language includes the outputs to
be asserted in lower-level layers and used for actuator
controls.
To implement the idea of subsumption, we let each
layer have "assumptions" about the inputs that may
later be adjusted by other (higher-level) layers. These
assumptions can take the form of an "abnormality"
Body
L1 input
Sensors
Output
Latches
Body
Sensors
Output
Latches
L2 input

Figure

3: A detailed look at two layers.
predicate ab i whose negation is a precondition for some
sentences in the language L I in the Body of that layer.
The assumptions can also take the form of the Closed-
World-Assumption (CWA), by minimizing a predicate
in L I . In all these minimizations we vary all of L to
make sure that our assumptions propagate. For exam-
ple, a higher-level layer can assert (in a lower-level layer)
the existence of an object that was previously excluded
(using our CWA).
During each cycle of any particular layer, we first
assert in that layer's Latches any sentences that higher
layers may have inferred (in the respective output language
for those higher layers). We then apply our "as-
sumptions" by circumscribing the ab predicates or input
predicates for which we enforce the CWA in the
theory while varying all other predicates and functions
in L. A theorem prover can then obtain the appropriate
outputs (for that layer), taking into account (as-
serted) interference from higher layers. More formally,
let Layer i be the theory of layer i, ab i the additional
"abnormality" constant symbol and C i a set of predicates
in L I , for which we wish to assert CWA. Then,
subsumption is achieved by using the parallel circumscription
policy
From an implementation point of view, many times this
formula can be substituted with a simple (external to
the logic) mechanical interference determining the value
of the minimized predicates; we discuss this issue in
section 4.
Semantics If we ignore the mechanism that runs behind
the scenes for a moment (e.g., ignore the time difference
between the theorem provers in different layers)
and consider the entire system of layers as one logical
theory, we can formalize the logical theory as follows.
Let Layer i , ab i , C i be as mentioned above. Then, the
combined system described above is equivalent to
Circ[Layer 0
Circ[Layer 1
3.3 A Model of Brooks' System
In this part we describe the logical theory corresponding
roughly to layers 0 and 1 in Brooks' Subsumption Ar-
chitecture. We divide our theory to conceptually correspond
to the layers and the modules mentioned in figure
1. For simplicity, we omit some parts of the description,
and refer the reader to appendix A.
Our layer 1 differs slightly from Brooks'. Instead of
implementing random wandering, this layer supports
simple movements towards a goal location. This goal
location is specified by layer 2 which, we can imagine,
first constructs a plan of exploration then, at each step
of this plan, asserts in the theory of layer 1 (via a subsumption
latch) where the next goal location is. Layer
1 makes a simple calculation to determine in which of
the eight quadrants surrounding it the goal position is
located (see Figure 4). Layer 1 then asserts in the theory
of layer 0 (by way of another subsumption latch)
the existence of a "virtual pushing object" in the opposing
quadrant. The avoidance capabilities of layer 0
effectively push the robot away from the object. The
robot heads in the direction of the goal although it may
deviate from a direct path, depending on the physical
objects in its vicinity.-3

Figure

4: Quadrants for the pushing object.
During each cycle of layer 0, the theorem prover of
layer 0 is asked to find the required actions for the modules
Turn and Forward described below. It attempts
to prove fwd(heading speed) and turn(heading angle),
where heading speed and heading angle are instantiated
by the proof. The results are translated into the appropriate
robot commands.
The inputs for this layer are the sonar data and the
output from Layer 1. The input language includes
the symbols sonar reading , sonar direction , Object ,
Direction, Distance, and halt robot . The output includes
fwd and turn.
Sonar The Sonar module takes the input from the
physical sonars, asserted in the form of the axiom
schema sonar reading(sonar dist , and
translates it to a map of objects (the type of each of
the symbols is defined in the appendix). 2
8dist
sonar reading(sonar
sonar direction(sonar
dist
sonar number
(1)
The reason we have only an implication from sonars
to objects is that we minimize Object in our circumscription
below. for the same reason, we don't include
axioms stating that there is at most one object at any
point.
Collide We take the predicate Object and check to
see if it has detected objects lying directly in front of
us.
Object Ahead =) halt robot
Object Ahead ()
(2)
Feelforce Feelforce does the dirty work of computing
the combined repulsive force from the different detected
objects 3 .
force direction
force x
force y
force
Runaway
:ab avoid =)
heading
:ab avoid =)
heading speed = force strength
We assume that the robot's 0 radians reference point
is straight ahead, the front sonar is numbered 0, and the
sonars are numbered consecutively counter-clockwise from
0 to NSONARS \Gamma 1.
3 Feelforce may be implemented as a library function
rather than as a logical theory, as it does not gain much
by the logical representation, it can be implemented more
efficiently as a procedure and the logical representation uses
some library functions anyway.
Turn
need turn(heading angle) =) turn(heading angle)
Forward
:halt robot - :need turn(heading angle)-
need fwd(heading speed) =)
fwd (heading speed)
need turn(heading angle) =) fwd(0)
Circumscribing the Theory
Finally, we add the parallel circumscription formula
The inputs for this layer are the current location
data from the robot and the output from
Layer 2. The input language includes the symbols
got move cmd and curr location. The output includes
Note that, unlike in layer 0, all the coordinates in
this layer are in terms of some fixed coordinate system
independent of the robot's location 4 .
Simple Move
pushing object(quadrant(x 0
Push
8quad: pushing object(quad) ()
Circumscribing the Theory
Again, we add the parallel circumscription formula
Implementation issues
We have implemented the above theory using the
PTTP theorem prover ((Stickel 1988b), (Stickel 1988a),
(Stickel 1992)) on a Sun Ultra60 Creator3D with
640MB RAM running Solaris 2.6 with Quintus Prolog
as the underlying interpreter for PTTP. The theory is
not yet implemented on a physical robot, yet the simulations
done on the above-described machine helped
us identify some points of difficulty in using a theorem
prover for the task of controlling an intelligent agent.
4 The robot is able to maintain its position in a cartesian
space with origin at the position where it was last "zeroed"
(e.g., where it was powered on).
4.1 Choice of a theorem prover
The first difficulty we encountered was in fact finding
a suitable theorem prover. Our theory includes several
mathematical computations (such as several trigonometric
functions (see the appendix A)) that are much
better suited for a systematic algorithm than a theorem
prover. Since we also wanted to have some algebraic
sophistication in our theory, we needed semantic
attachments. We examined many theorem provers and
none of them seemed to support semantic attachments
easily, nor did we have any convenient control over the
theorem proving process (via strategies or otherwise).
Some of the provers that we examined more closely
are Otter 5 (a resolution theorem prover), ACL2 6 (an
industrial-strength version of the Boyer Moore theorem
prover) and ATP 7 (a model elimination theorem
prover). The major difficulties we encountered with
them (not all difficulties were encountered with all)
were the inability to append semantic attachments eas-
ily, complexity of making the theorem prover run on
a given platform, the inability to control the inference
process easily, and the lack of documentation.
In addition we also examined a few proof checkers
such as PVS 8 (a proof checker), HOL 9 and GETFOL 10 ,
all of which were found unsuitable due to their need for
at least some human intervention.
PTTP (Prolog Technology Theorem Prover) is a
model-elimination theorem prover. Given a theory
made of clauses (not necessarily disjunctive) without
quantifiers, the PTTP produces a set of PROLOG-like
horn clauses, it makes sure only sound unification is
produced and avoids the negation-as-failure proofs that
are produced by the PROLOG inference algorithm. It
also makes sure the inference algorithm is complete by
using ID (Iterative Deepening) in the proof space. Together
these ensure the PTTP is a sound and complete
theorem prover.
One of the features that we liked the most about the
PTTP was that, despite the lack of suitable documentation
(although there are a fair number of examples),
the theorem prover is very easy to customize and its reliance
on the underlying language (it was implemented
in both PROLOG and LISP) allows the easy use of
semantic attachments. The collection of examples together
with the PTTP software is very illustrative and,
despite some difficulties incurred by the use of semantic
attachments and built-in predicates (such as the algebraic
gave us relatively few troubles in
either installation or use.
6 http://www.cs.utexas.edu/users/moore/acl2/acl2-
doc.html
manual.html
9 http://www.comlab.ox.ac.uk/archive/formal-
methods/hol.html
4.2 Running PTTP with our theory
We embodied the Feelforce module in a C function
get force that needs no input and returns the force vector
[Strength; Direction]. It does its work by calling
the prolog bagof operator to collect all the objects for
which existence proofs can be found and then simply
computes the sum of the forces subjected by each of
the objects. The CWA (Closed World Assumption) is
achieved here by limiting the sizes of proofs to be no
longer than a specified constant (we experimented a little
and got the constant to be 20. At about 16 all the
objects had a proof. At around 36 all the objects got a
second proof and the same happened at about 48. We
did not experiment further).
Finally, get force(L); !; =!;+;  ; abs and others are
treated as "built-in" functions/predicates and are given
to the underlying prolog for evaluation (which in turn
may call the C function get force for the prolog pred-
icate). This way one manages to get the semantic attachments
without the need to be able to prove many
properties of algebraic formulas.
The rest of the theory stays the same, with the provision
that constants such as NSONARS and MIN DIST
are incorporated with the aid of predicates such as
nsonars(X) and min dist(Y ).
We ran our theory with different simulated sensory
inputs (results from a sample run are shown in figures 5,
7, and 6 in the appendix) and the results were achieved
in 0.2 to 0.3 seconds, depending on whether a turn was
needed (leaning towards 0.2 seconds) or a forward move
was needed (leaning mostly towards 0.3 seconds). It is
worth mentioning that in the computation of get force
we applied caching (of the computed force), and since
PTTP does not apply caching of results, there was a
major improvement in efficiency (from several seconds
for a proof to 0.2-0.3) using this simple scheme. This is
due to the fact that every proof "re-proved" get force
many times.
4.3 Nonmonotonicity considerations
As mentioned above, the way we treated nonmonotonicity
in this experiment was using NAF (Negation-as-
Failure). If a default was not proved to be wrong after
a certain amount of time, then we treated it as false. In
particular, there were three points in which nonmonotonicity
was required:
1. CWA for the objects in our world.
2. halt robot was assumed to be false unless otherwise
proved.
3. ab avoid , which allows complete overriding of the force
constraints input of layer 0 by layer 1, is assumed to
be false, since we did not use that facility (overriding)
in our implementation of level 1.
For the CWA for the objects, we looked for proofs no
longer than 20 and we did the same for the halt robot
proposition.
5 Related Work
In our work we showed that theorem provers can be
used to implement robot control. We also showed that
an extended version of Brooks' Subsumption Architecture
can be implemented using theorem provers and
logical theories. This extended version is proposed as a
general architecture for building intelligent agents. Notice
that we did not include a specific action theory
above L0, but only showed how can such a theory influences
L0.
We compare our work to those of Shanahan ((Shana-
han 1996), (Shanahan 1998)), Baral and Tran ((Baral &
Tran 1998)) and Reiter et al ((Reiter 1998), (Lesprance
et al. 1996), (Reiter 1996)): (Shanahan 1998) describes
a map-building process using abduction. His abduction
is specialized for the specific scenario of spatial occupancy
and noise that one may wish to include. He then
implements the theory in an algorithm that abides by
the logical theory, and to his account of abduction.
In contrast, our work is not implemented in an algorithm
but rather using a general-purpose theorem
prover. We showed that we can use theorem provers
for control as long as the theory remains small and relatively
simple. We described a way of joining such theorem
provers and theories in a structure that allows
for larger theories to interact and for more complicated
behaviors to be established.
Although our control theory is much simpler than
that of (Shanahan 1998), we can in fact include a version
of the original theory presented by Shanahan as an
upper layer. Also, since our robot is a more sophisticated
mobile robot, any inclusion of such a theory will
have to take into account the different sensors (sonars
instead of switches).
The work of Baral and Tran ((Baral & Tran 1998))
focuses on the relationship between the members of
the family of action languages A ((Gelfond & Lifschitz
1993), (Giunchiglia, Kartha, & Lifschitz 1997), (Kartha
reactive control modules. They
define control modules to be of a form of Stimulus-Response
(S-R) agents (see (Nilsson 1998)) where a
state is defined by a set of fluent values (either sensory
or memory) and a sequence of rules defines the
action that the agent should take, given conditions on
the state. They provide a way to check that an S-R
module is correct with respect to an action theory in A
or AR. Finally, they provide an algorithm to create an
S-R agent from an action theory.
Their work, although dealing with reactivity, does
not seem to be able to deal with the world-complexity
of our model. Our sensors have too many possible input
values to be accounted for by several input fluents. If
one decides to use the algorithm described by Baral and
Tran to produce a simple S-R module, the complexity
of the algorithm (which is worst-case exponential in the
number of fluents) will not allow it to end in our life
time. Also, they lack the hierarchy-of-theories model
that we use in our work.
Finally, the work of Reiter, Levesque and their colleagues
((Levesque et al. 1997), (Giacomo, Lesper-
ance, & Levesque 1997), (Reiter 1998), (Lesprance et al.
1996), (Reiter 1996), (Giacomo, Reiter, & Soutchanski
1998)) focuses on the language GOLOG (and its vari-
ants) for the specification of high-level robot actions. In
their paradigm, there is a planner that computes/plans
the GOLOG program off-line, then lets the robot execute
the GOLOG program on-line. Their language
includes (among others) testing for a truth condition,
performing a primitive action, performing a sequence of
actions, a nondeterministic choice of two actions and a
nondeterministic iteration.
While we use a hierarchical model for reasoning,
merging both planning and execution, their work splits
planning and execution, having the planning done off-
line. Also, their use of logic is only for the semantics of
their GOLOG programs, which is given using Situation
Calculus ((McCarthy & Hayes 1969)).
6 Discussion and Future Work
In the last 5 years, the logical approach to AI got reinvigorated
with positive results on different frontiers,
from planning (e.g., the work of Bibel and of Selman
and Kautz ((Kautz, McAllester, & Selman 1996))) to
sensing and AI architectures (e.g., (Shanahan 1996),
(Lesperance et al. 1994), (Giacomo, Lesperance, &
Levesque 1997)).
In this paper, we have presented a logic-based architecture
that formalizes Brooks' Subsumption Architec-
ture, using circumscription to implement subsumption.
In so doing, we have combined the reactivity advantages
of Brooks' architecture with the declarative advantages
of logic to produce a first cut at an architecture that
can perform sensing, planning and acting concurrently.
At the moment, the system is only partially implemented
(level 0 only) on a simulating computer.
Besides implementing the system on a mobile robot,
our future work plan includes expanding the layers described
in this paper to contain planning layers, map-
creating layers (e.g., creating a map of the world (pos-
sibly following the work of Shanahan)), layers that contain
beliefs about the world (e.g., we may want to doubt
our conclusion that we are in a certain location if we
believe that a moment ago we were in a distant location
and no reasonable change was done to the world to put
us in that new location), etc. This project also serves
as an experiment in the Elaboration Tolerance of the
layering approach.

Acknowledgments

We wish to thank Mark Stickel for allowing us to use
his PTTP sources (both for PROLOG and LISP) and
providing helpful answers to our inquiries regarding its
use.
This research was supported by an ARPA (ONR)
grant N00014-94-1-0775 and by a National Physical Science
Consortium (NPSC) fellowship.



--R

Reasoning.
Relating theories of actions and reactive control.
Nonmonotonic Reasoning: An Overview
Nonmonotonic Reasoning: Logical Foundations of Common Sense.
A robust layered control system for a mobile robot.

Representing Actions and Change by Logic Programs.

Reasoning about concurrent execution

Execution monitoring of high-level robot pro- grams

Indeterminacy and Ramifica- tions
Actions with indirect effects: Preliminary report.

Encoding plans in propositional logic.
A logical approach to high-level robot programming: A progress report
In Kuipers
Foundations of a logical approach to agent programming.
Golog: A logic programming language for dynamic domains.
Some Philosophical Problems from the Standpoint of Artificial Intel- ligence
Programs with Common Sense.
In Mechanisation of Thought Processes

Formalization of common sense
Elaboration Tol- erance
The Society of Mind.
Artificial Intelligence
Reasoning under uncertainty.
Natural actions
Knowledge in Action: Logical Foundations for Describing and Implementing Dynamical Systems.
Features and Fluents.
Robotics and the common sense informatic situation.
Solving the Frame Problem
A logical account of the common sense informatic situation for a mobile robot.
Postmodular systems: Architectural principles for cognitive robotics.

th International Conference on Automated Deduc- tion
A Prolog Technology Theorem Prover: implementation by an extended Prolog compiler.
A Prolog Technology Theorem Prover: a new exposition and implementation in Prolog.
A The Logical Theory In this appendix we draw the entire logical theory for our version of Brooks' Subsumption Architecture example from (Brooks



Objects: obj
sonar number



"sum the forces"






search for cost 1 proof.
search for cost 2 proof.
search for cost 3 proof.
Proof: Goal
1222 inferences in 0.02 seconds

Proof: Goal
36 need-turn(-314) :- [6]
12664 inferences in 0.24 seconds
--TR
Applications of circumscription to formalizing common-sense knowledge
Automated deduction by theory resolution
The society of mind
A Prolog technology theorem prover: implementation by an extended Prolog computer
On the relationship between circumscription and negation as failure
Principles of metareasoning
The frame problem in situation the calculus
A Prolog technology theorem prover
Introduction to HOL
A situated view of representation and control
Building brains for bodies
Representing action
An Behavior-based Robotics
Computer-Aided Reasoning
Reinventing shakey
Interpolation Theorems for Nonmonotonic Reasoning Systems
Logic-Based Subsumption Architecture
Spatial Agents Implemented in a Logical Expressible Language
Efficient Approximation for Triangulation of Minimum Treewidth
Decision-Theoretic, High-Level Agent Programming in the Situation Calculus
cc-Golog
High-Level Robot Control through Logic
A Prolog Technology Theorem Prover
Layered and Resource-Adapting Agents in the RoboCup Simulation
Dynamic Subsumption Architecture for Programming Intelligent Agents
cognitive robotics;subsumption architecture;logical representations