Deciding Regular Grammar Logics with Converse through First-Order Logic

de Nivelle, Hans; Demri, Stéphane

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Journal Article

Deciding Regular Grammar Logics with Converse through First-Order Logic

MPS-Authors

/persons/resource/persons44298

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

Citation

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

Abstract

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.