SCSS 2008 Austrian-Japanese Workshop on Symbolic Computation in Software Science, RISC-Linz Report Series vol:08-08 pages:16-30
Symbolic Computation in Software Science Austrian-Japanese Workshop, SCSS 2008 location:RISC, Castle of Hagenberg, Austria date:12-13 July 2008
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, 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 applications of the system.