The two-variable guarded fragment with transitive relations
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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 non-unary relations to occur only in guards, the logic becomes decidable. The latter subclass of the guarded fragments the one that occurs naturally when translating multi-modal logics of the type Kg/sub 4/ S/sub 4/ or S5 into first-order logic. We also show that the loosely guarded fragment without equality and with a single transitive relation is undecidable.Keywords
This publication has 15 references indexed in Scilit:
- A superposition decision procedure for the guarded fragment with equalityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- On the Restraining Power of GuardsThe Journal of Symbolic Logic, 1999
- On logics with two variablesTheoretical Computer Science, 1999
- Guarded fixed point logicPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1999
- On the Decision Problem for Two-Variable First-Order LogicBulletin of Symbolic Logic, 1997
- The unsolvability of the Gödel class with identityThe Journal of Symbolic Logic, 1984
- The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems)Published by Springer Nature ,1984
- Propositional dynamic logic of regular programsJournal of Computer and System Sciences, 1979
- On languages with two variablesMathematical Logic Quarterly, 1975
- Decidability of Second-Order Theories and Automata on Infinite TreesTransactions of the American Mathematical Society, 1969