The knowledge representation community has often stressed the primacy of first order logic, as a maximal sound and complete system. The results of this paper show that another strictly incomparable system, monadic second order logic (which is sound, complete, and decidable), is more natural in A.I.'s most classic domains, reasoning about action, non-monotonicity, and blocksworld.
The situation calculus is a classic logical A.I. domain. However, it contains binary predicates, and thus determining theoremhood is possibly undecidable. Its now standard formalization contains second order logic, to state induction over situations, and thus might be highly undecidable.
The classic domain of logical A.I., blocksworld, is not axiomatizable in first order logic. We present a sound and complete axiomatization of all its domain constraints---we are unaware of a previous completeness proof.
The projection problem has also been attacked with second order logic, via circumscription. Though the basic situation calculus might be axiomatizable, these solutions could make theoremhood highly undecidable.
In all these cases we show that the problem of theoremhood remains decidable by embedding in monadic second order logic.
By: Tom Costello
Published in: RJ10272 in 2002
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .