Soundness and Completeness Theorems for Three Formalizations of Action

Abstract

Instead of trying to compare methodologies for reasoning about action on the basis of specific examples, we focus here on a general class of problems, expressible in a declarative language A. We propose three translations, P, R and B from A, representing respectively the first order methods of reasoning about action proposed by Pednault and Reiter and the circumscriptive approach of Baker. We then prove the soundness and completeness of these translations relative to the semantics of A. This lets us compare these three methods in a mathematically precise fashion. Moreover, we apply the methods of Baker in a general setting and prove a theorem which shows that if the domain of interest can be expressed in A, circumscription yields results which are intuitively expected.