Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
  Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben
Konferenzbeitrag

The Two-Variable Guarded Fragment with Transitive Relations

MPG-Autoren
/persons/resource/persons44474

Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44784

Meyer,  Christoph
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45662

Veanes,  Margus
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Ganzinger, H., Meyer, C., & Veanes, M. (1999). The Two-Variable Guarded Fragment with Transitive Relations. In G. Longo (Ed.), Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS-99) (pp. 24-34). Los Alamitos, USA: IEEE.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-000F-36A6-0
Zusammenfassung
We consider the restriction of the guarded fragment to the two-variable case where, in addition, binary relations may be specified as transitive. We show that (i) this very restricted form of the guarded fragment without equality is undecidable and that (ii) when allowing transitive relations other than equality to occur only in guards, the logic becomes decidable. The latter subclass of the guarded fragment is the one that occurs naturally when translating multi-modal logics of the type K4, S4 or S5 into first-order logic. We also show that the loosely guarded fragment with a single transitive relation is undecidable.