Journal of Symbolic Logic 64 (4):1719-1742 (1999)

Abstract
Guarded fragments of first-order logic were recently introduced by Andreka, van Benthem and Nemeti; they consist of relational first-order formulae whose quantifiers are appropriately relativized by atoms. These fragments are interesting because they extend in a natural way many propositional modal logics, because they have useful model-theoretic properties and especially because they are decidable classes that avoid the usual syntactic restrictions (on the arity of relation symbols, the quantifier pattern or the number of variables) of almost all other known decidable fragments of first-order logic. Here, we investigate the computational complexity of these fragments. We prove that the satisfiability problems for the guarded fragment (GF) and the loosely guarded fragment (LGF) of first-order logic are complete for deterministic double exponential time. For the subfragments that have only a bounded number of variables or only relation symbols of bounded arity, satisfiability is EXPTIME-complete. We further establish a tree model property for both the guarded fragment and the loosely guarded fragment, and give a proof of the finite model property of the guarded fragment. It is also shown that some natural, modest extensions of the guarded fragments are undecidable
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2586808
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 55,856
Through your library

References found in this work BETA

On Languages with Two Variables.Michael Mortimer - 1975 - Mathematical Logic Quarterly 21 (1):135-140.
Undecidability Results on Two-Variable Logics.Erich Grädel, Martin Otto & Eric Rosen - 1999 - Archive for Mathematical Logic 38 (4-5):313-354.
On Preservation Theorems for Two-Variable Logic.Erich Gradel & Eric Rosen - 1999 - Mathematical Logic Quarterly 45 (3):315-325.

View all 6 references / Add more references

Citations of this work BETA

Decidable Fragments of First-Order Temporal Logics.Ian Hodkinson, Frank Wolter & Michael Zakharyaschev - 2000 - Annals of Pure and Applied Logic 106 (1-3):85-134.
Modal and Guarded Characterisation Theorems Over Finite Transition Systems.Martin Otto - 2004 - Annals of Pure and Applied Logic 130 (1-3):173-205.

View all 19 citations / Add more citations

Similar books and articles

Guarded Fragments with Constants.Balder ten Cate & Massimo Franceschet - 2005 - Journal of Logic 14 (3):281-288.
Guarded Fragments with Constants.Balder ten Cate & Massimo Franceschet - 2005 - Journal of Logic, Language and Information 14 (3):281-288.
Guards, Bounds, and Generalized Semantics.Johan van Benthem - 2005 - Journal of Logic, Language and Information 14 (3):263-279.
Deciding Regular Grammar Logics with Converse Through First-Order Logic.Stéphane Demri & Hans De Nivelle - 2005 - Journal of Logic, Language and Information 14 (3):289-329.
A Guarded Fragment for Abstract State Machines.Antje Nowack - 2005 - Journal of Logic, Language and Information 14 (3):345-368.

Analytics

Added to PP index
2009-01-28

Total views
205 ( #44,304 of 2,401,764 )

Recent downloads (6 months)
1 ( #551,897 of 2,401,764 )

How can I increase my downloads?

Downloads

My notes