Tableau - based bisimulation invariance testing

• Autorzy: Perkov T.
• Języki publikacji: EN

Abstrakty

EN

A tableau procedure that tests bisimulation invariance of a given first-order formula, and therefore tests if that formula is equivalent to the standard translation of some modal formula, is presented. The test is sound and complete: a given formula is bisimulation invariant if and only if there is a closed tableau for that formula. The test generally does not terminate, but it does if a given formula is bisimulation invariant, i.e., the test is positive.

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2013
• Tom: Vol. 48
• Strony: 101--115
• Opis fizyczny: Bibliogr. 6 poz., rys.

Twórcy

autor

Perkov T.

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

Bibliografia

• [1] J. Blackburn, M. de Rijke, Y. Venema, Modal Logic, Cambridge University Press, 2001.
• [2] G. Boolos, Trees and Finite Satisfiability: Proof of a Conjecture of Burgess, Notre Dame Journal of Formal Logic 25 (1984), pp. 193-197.
• [3] H.-D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic, Springer-Verlag, 1984.
• [4] R. Jeffrey, J. P. Burgess, Formal Logic: Its Scope and Limits, Hackett, 2006.
• [5] R. M. Smullyan, First-Order Logic, Springer-Verlag, 1968.
• [6] J. van Benthem, Exploring Logical Dynamics, Studies in Logic, Language and Information, CSLI Publications & FoLLI, Stanford, 1996.