Dividing and conquering logic

摘要

This thesis provides principles for knowledge representation and reasoning with logical theories that are composed from fragments. It provides algorithms for reasoning with logical theories that are made of multiple partitions that may overlap in contents. Algorithms for automatic decomposition of given theories to partitions are proposed. Some of these algorithms are shown to approximate the optimum by a small constant factor. An architecture for an intelligent agent that uses similar algorithms and follows Brooks' subsumption architecture using logic is examined. Experiments applying this architecture for the task of mobile-robot control are reported. Finally, following the object-oriented design methodology, tools and methodology for the design of decomposed theories are provided. The tools and methodology are applied for the design of logical theories describing the domain of robot motion and interaction.