A Revised Tactic Semantics for the Tableau Work Bench


Kelly, J.


Department of Computer Science, Australian National University, Canberra, Australia, p.74 (2009)


The Tableau Work Bench (TWB) provides a user-friendly framework for building automated tableau-based theorem provers. Its target audience includes researchers who want to experiment with automated reasoners for calculi that they are designing. The TWB allows them to do so even with limited programming experience. An important consideration when designing a tableau calculus for a logic is the order of rule applications. Incorrectly ordering rule applications can cause a calculus to become unsound, incomplete or non-terminating. The TWB addresses this by implementing a tactic language based on the language "Angel" described by [Martin et al. 1996], but the semantics of this language in the context of the TWB are not completely specified and are not expressive enough in certain instances. In this thesis, we restrict the notion of a tableau rule in order to provide well-defined semantics for rule application and tactic evaluation. We also provide a sample implementation of our rule and tactic system in O'Caml but leave its integration into the TWB as further work. We also defer the proofs that the implementation meets its specification and that the specified system is equivalent to a corresponding naive tableau procedure.
thesis.pdf277.03 KB