Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics

Minica, S. and Khodadadi, M. and Tishkovsky, D. and Schmidt, R. A. (2013)

This paper presents two tableau provers for deciding interrogative-epistemic logics. They are both based on a tableau calculus generated using a recently introduced tableau synthesis framework. We have implemented the calculus using two approaches, namely MetTeL2 and Qtab.lhs. Here, we describe and compare these different approaches of implementing a tableau procedure.