Tractable Closed World Reasoning with Updates

Closed world reasoning is the process of inferring that a logical sentence is false based on its absence from a knowledge base, or the inability to derive it. Previous work on circumscription, autoepistemic logic, and database theory has explored logical axiomatizations of closed world reasoning, and investigated computational tractability for propositional theories. Work in planning has traditionally made the closed world assumption but has avoided closed world reasoning. We take a middle position, and describe a tractable method for closed world reasoning over the schematized theories of action used by planning algorithms such as NONLIN, TWEAK, and UCPOP. We show the method to be both sound and tractable, and incorporate it into the XII planner [Golden et al. , 1994]. Experiments utilizing our softbot (software robot) demonstrate that the method can substantially improve its performance by eliminating redundant information gathering.