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

Tin Perkov; Luka  Mikec

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

Publication date: 10.11.2021

Reports on Mathematical Logic, 2021, Number 56, pp. 57-74

https://doi.org/10.4467/20842589RM.21.003.14375

Authors

Download full text

PDF

Titles

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

Abstract

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.

Keywords

and phrases: modal logic, bisimulation invariance, tableaux

References

Download references

[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.

Information

Information: Reports on Mathematical Logic, 2021, Number 56, pp. 57-74

DOI: https://doi.org/10.4467/20842589RM.21.003.14375

Article type: Original article

Authors

Tin Perkov

Polytechnic of Zagreb Avenija V. Holjevca 15 10000 Zagreb, Croatia

Luka Mikec

Department of Mathematics, Faculty of Science, University of Zagreb, Bijenicka c. 30, HR-10000 Zagreb, Croatia

Published at: 10.11.2021

Received at: 19.01.2021

Article status: Open

Licence: CC BY-NC-ND

Percentage share of authors:

Tin Perkov (Author) - 50%

Luka Mikec (Author) - 50%

Classification number:

AMS:

Modal logic (including the logic of norms) (03B45)

Article corrections:

Publication languages:

English

View count: 912

Number of downloads: 803

<p>Tableau-based translation from first-order logic to modal logic</p>

Download xml