The LSA is 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 circumscription to
make assumptions in lower layers, and nonmonotonically retract them
when higher layers draw new conclusions. The semantics of such an
approach may be given by Circumscription. At the moment, this
project describes four layers designed for the task of robot
control and an experiment that empirically shows the feasibility of
using fully expressive FOL theorem provers for robot control with our
E. Amir and P. Maynard-Reid II,
LSA Version 2.0, now available.
LSA software and logical theories for controlling a mobile robot.
This is a tested system for realtime control of a Nomad 200 mobile
robot in an office environment. All of the layers are implemented using
Mark Stickel's PTTP theorem prover. (November 2001)
Also available, is the log of one of our experiments.