English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Conference Paper

The Two-Variable Guarded Fragment with Transitive Relations

MPS-Authors
/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;

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

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.


Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-36A6-0
Abstract
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.