Complexity Results for First-Order Two-Variable Logic with Counting

DOI10.1137/S0097539797323005zbMath0956.03039OpenAlexW1971102936MaRDI QIDQ4943858

Wiesław Szwast, Leszek Pacholski, Lidia Tendera

Publication date: 19 March 2000

Published in: SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1137/s0097539797323005

zbMATH Keywords

computational complexityfirst-order logiccountingsatisfiability problemdecision problemNEXPTIME-completefirst-order sentences

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Related Items

The guarded fragment with transitive guards, Data-complexity of the two-variable fragment with counting quantifiers, A family of dynamic description logics for representing and reasoning about actions, A description logic based situation calculus, Undecidable Propositional Bimodal Logics and One-Variable First-Order Linear Temporal Logics with Counting, Deciding expressive description logics in the framework of resolution, CTL Model-Checking with Graded Quantifiers, A resolution-based decision procedure for \({\mathcal{SHOIQ}}\)., A tableau decision procedure for \(\mathcal{SHOIQ}\), One-variable logic meets Presburger arithmetic, The complexity of finite model reasoning in description logics, Complexity of the two-variable fragment with counting quantifiers, Regular Graphs and the Spectra of Two-Variable Logic with Counting