de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

Deciding Regular Grammar Logics with Converse through First-Order Logic

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44298

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-262F-5
Zusammenfassung
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.