Special University Oral Examination
*******************************************************************
Dividing and Conquering Logic
Eyal Amir
Department of Computer Science
Stanford University
Gates Building, Room 104
Friday, June 1, 2001
10:00 AM - 11:00 AM
(Refreshments served at 9:45 AM)
*******************************************************************
Abstract
Logical theories can be used in many tasks, such as planning,
diagnosis, reasoning about beliefs of agents, natural language
processing, common-sense reasoning, and modeling and reasoning about
logical circuits and computer programs. However, building large
logical knowledge bases and automatically reasoning with them is often
difficult and slow. In addition, the integration of large logical
knowledge bases usually requires all knowledge bases to agree on a
particular reasoning procedure, or give up completeness.
In this talk I will describe an approach for representation and
reasoning with logical theories that are made of multiple partitions
that may overlap in contents. The reasoning algorithms are sound and
complete for FOL and propositional logic. They allow multiple
knowledge bases to collaborate in finding conclusions and answering
queries even if they use different theorem provers and different
reasoning procedures. Also, we can speed-up reasoning with a given
theory if it is partitioned prior to reasoning, either by hand (e.g.,
using object-oriented design techniques) or automatically. I will
show how the methodology and tools used for object-oriented design
can be applied to logical theories.
To automatically partition a theory, we reduce the theory to a graph
and find a tree decomposition in the graph (this is equivalent to
finding clique trees and finding triangulations of minimum treewidth).
I will describe algorithms for automatic decomposition of given
theories to partitions that are shown to approximate the optimum by a
small constant factor, and are significantly faster that previous
algorithms. These algorithms allow us to partition large knowledge
bases and triangulate large Bayes networks. I will conclude with an
architecture for an intelligent agent that uses similar algorithms and
follows Brooks' subsumption architecture using logic. The architecture
was implemented for a Nomad200 mobile robot, and the experiments that
we performed with this system will be described in the talk.
+----------------------------------------------------------------------------+
| This message was sent via the Stanford Computer Science Department |
| colloquium mailing list. To be added to this list send an arbitrary |
| message to colloq-subscribe@cs.stanford.edu. To be removed from this list,|
| send a message to colloq-unsubscribe@cs.stanford.edu. For more information,|
| send an arbitrary message to colloq-request@cs.stanford.edu. For directions|
| to Stanford, check out http://www-forum.stanford.edu |
+-------------------------------------------------------------------------xcl+