Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics

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

In Fontaine, P. and Schmidt, R. A. and Schulz, S. (eds), PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning. EPiC Series, Vol. 21 EasyChair, 109-123. BiBTeX, Link to EasyChair Proceedings.

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.

Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 16 Oct 14
Copyright © 2012 Renate A. Schmidt, School of Computer Science, Man Univ,