Tableau-based translation from first-order logic to modal logic

Tin Perkov,

Luka Mikec


We define a procedure for translating a given first-order formula to an equivalent modal formula, if one exists, by using tableau-based bisimulation invariance test. A previously developed tableau procedure tests bisimulation invariance of a given first-order formula, and therefore tests whether that formula is equivalent to the standard translation of some modal formula. Using a closed tableau as the starting point, we show how an equivalent modal formula can be effectively obtained.

AMS subject classification: 03B45.

Słowa kluczowe: and phrases: modal logic, bisimulation invariance, tableaux

[1] J. van Benthem, Exploring Logical Dynamics, Studies in Logic, Language and Information, CSLI Publications & FoLLI, Stanford, 1996.

[2] P. Blackburn, M. de Rijke, Y. Venema, Modal Logic, Cambridge University Press, 2001.

[3] G. Boolos, Trees and Finite Satisfiability: Proof of a Conjecture of Burgess, Notre Dame Journal of Formal Logic 25 (1984), 193-197.

[4] T. Brauner, Hybrid Logic and its Proof-Theory, Springer, 2011.

[5] J. Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009.

[6] T. Perkov, Tableau-based bisimulation invariance testing, Reports on Mathematical Logic 48 (2013), 101-115.

[7] R. M. Smullyan, First-Order Logic, Springer-Verlag, 1968.