An Automated Tableau Theorem Prover for FO(ID)

Abstract. Inductive definitions are frequently encountered in software, underlying many common program and algorithm components, such as recursive functions and loops. Therefore, in disciplines such as program verification or specification extraction, it is important to be able to rep-resent and reason with inductive definitions in a formal way. Ideally our formal representation language would extend classical logic and take ad-vantage of the powerful symbolic proof systems that exist for it. FO(ID) is a language that extends classical logic with inductive definitions, which are captured by the well-founded semantics of logic programming. In this paper we present an automated tableau theorem prover for FO(ID), which has the potential to be of much use in the application of symbolic proof techniques to software science. We describe the tableau rules and their implementation, and discuss some possible extensions and applica-tions of the system.