6533b85ffe1ef96bd12c279e

RESEARCH PRODUCT

The guarded fragment with transitive guards

Wiesław SzwastLidia Tendera

subject

Mathematical logicDiscrete mathematicsCombinatoricsTransitive relationComputational complexity theoryLogicBounded functionDecision problemPredicate (grammar)First-order logicDecidabilityMathematics

description

The guarded fragment with transitive guards, (GF+TG), is an extension of the guarded frag- ment of 9rst-order logic, GF, in which certain predicates are required to be transitive, transitive predicate letters appear only in guards of the quanti9ers and the equality symbol may appear everywhere. We prove that the decision problem for (GF+TG) is decidable. Moreover, we show that the problem is in 2EXPTIME. This result is optimal since the satis9ability problem for GF is 2EXPTIME-complete (J. Symbolic Logic 64 (1999) 1719-1742). We also show that the satis- 9ability problem for two-variable (GF+TG) is NEXPTIME-hard in contrast to GF with bounded number of variables for which the satis9ability problem is EXPTIME-complete. c 2004 Elsevier B.V. All rights reserved. MSC: 03D15; 68Q17; 03B10; 03B25

yearjournalcountryeditionlanguage
2004-08-01Annals of Pure and Applied Logic
10.1016/j.apal.2004.01.003http://dx.doi.org/10.1016/j.apal.2004.01.003