Eyal Amir Computer Science Department University of Illinois, Urbana-Champaign http://www.cs.uiuc.edu/~eyal
Abstract
Logical theories (e.g., first-order logic (FOL) and propositional) can be used in many tasks, such as diagnosis, planning, reasoning about beliefs of agents, natural language processing, 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 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. Also, we can speed-up reasoning with a given theory if it is partitioned prior to reasoning, either by hand or automatically. I will present algorithms that partition a theory automatically in a way that approximates the optimal (minimizing expected time for reasoning). I will conclude with applications of this approach to intelligent agent architectures (particularly, mobile-robot control), AI planning, and compact propositionalizations of FOL theories.