Harald Ganzinger, Christoph Meyer, and Margus Veanes
We consider the restriction of the guarded fragment to the two-variable case where, in addition, binary relations may be specied as transitive. We show that (i) this very restricted form of the guarded fragment without equality is undecidable and that (ii) when allowing non-unary relations 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 rst-order logic. We also show that the loosely guarded fragment without equality and with a single transitive relation is undecidable.
In LICS 1999
Publisher IEEE Computer Society
Copyright © 2007 IEEE. Reprinted from IEEE Computer Society. This material is posted here with permission of the IEEE. Internal or personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution must be obtained from the IEEE by writing to email@example.com. By choosing to view this document, you agree to all provisions of the copyright laws protecting it.