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 represent and reason with inductive definitions in a formal way. Ideally our formal representation language would extend classical logic and take advantage of the powerful symbolic proof systems that exist for it. FO(ID) is a language that extends classical logic with inductive definitions, whichare 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 andtheir implementation, and discuss some possible extensions and applications of the system.
展开▼
