Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Journal Article

Deciding Regular Grammar Logics with Converse through First-Order Logic


de Nivelle,  Hans
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

de Nivelle, H., & Demri, S. (2005). Deciding Regular Grammar Logics with Converse through First-Order Logic. Journal of Logic, Language and Information, 14, 289-329.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-262F-5
We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting, because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing these frame conditions. It is practically relevant, because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with converse. The class of regular grammar logics includes numerous logics from various application domains. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2, without extra machinery, as for example fixed point operators.