hide
Free keywords:
-
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.
