Aiming to pinpoint the reasons behind the decidability of some complex extensions of modal logic, we propose a new classification criterion for sentences of first-order logic, which is based on the kind of binding forms admitted in their expressions, i.e., on the way the arguments of a relation can be bound to a variable. In particular, we describe a hierarchy of four fragments focused on the Boolean combinations of these forms, showing that the less expressive one is already incomparable with several first-order limitations proposed in the literature, as the guarded and unary negation fragments. We also prove, via a novel model-theoretic technique, that our logic enjoys the finite-model property, Craig's interpolation, and Beth's definability. Furthermore, the associated model-checking and satisfiability problems are solvable in PTime and Sigma_3^P, respectively.
@InProceedings{mogavero_et_al:LIPIcs.CSL.2015.648, author = {Mogavero, Fabio and Perelli, Giuseppe}, title = {{Binding Forms in First-Order Logic}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {648--665}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.648}, URN = {urn:nbn:de:0030-drops-54443}, doi = {10.4230/LIPIcs.CSL.2015.648}, annote = {Keywords: First-Order Logic, Decidable Fragments, Satisfiability, Model Checking} }
Feedback for Dagstuhl Publishing