Title: An automated tableau theorem prover for FO(ID)
Authors: Bond, Stephen ×
Denecker, Marc #
Issue Date: Jul-2008
Host Document: SCSS 2008 Austrian-Japanese Workshop on Symbolic Computation in Software Science, RISC-Linz Report Series vol:08-08 pages:16-30
Conference: Symbolic Computation in Software Science Austrian-Japanese Workshop, SCSS 2008 location:RISC, Castle of Hagenberg, Austria date:12-13 July 2008
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 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.
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
tableau_paper.pdf Accepted 192KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.