Abate, P., Goré, R., & Widmann, F (2007). Cut-free Single-pass Tableaux for the Logic of Common Knowledge. Workshop on Agents and Deduction at TABLEAUX.

Fitting, M., & Mendelsohn, R. L. (1999). First-order modal logic. Kluwer Academic Publishers.

LoTREC Generic Tableau prover (http://www.irit.fr/Lotrec/)

van der hoek, W., & Meyer, J. Ch. (2004). Epistemic Logic for AI and Computer Science. Cambridge University Press.

van der Vaart, E., & van Valkenhoef, G. (2007). OOPS: An Automated Proof Tool for S5n. Unpublished.