6533b828fe1ef96bd1288d2a

RESEARCH PRODUCT

On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity

Lidia TenderaWiesław Szwast

subject

CombinatoricsDiscrete mathematicsTransitive relationTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESPhraseComputational complexity theoryComputer Science::Logic in Computer SciencePredicate (mathematical logic)Decision problemBoolean satisfiability problemSentenceDecidabilityMathematics

description

We study the finite satisfiability problem for the guarded fragment with transitivity. We prove that in case of one transitive predicate the problem is decidable and its complexity is the same as the general satisfiability problem, i.e. 2Exptime-complete. We also show that finite models for sentences of GF with more transitive predicate letters used only in guards have essentially different properties than infinite ones.

yearjournalcountryeditionlanguage
2005-01-01
https://doi.org/10.1007/11591191_22