2026-07-23T15:54:47Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5444 2024-03-06T10:36:28Z ddc:004 open_access

Binding Forms in First-Order Logic Mogavero, Fabio Perelli, Giuseppe First-Order Logic Decidable Fragments Satisfiability Model Checking 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Fabio Mogavero and Giuseppe Perelli 2015 Is Part Of LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2015.648 urn:nbn:de:0030-drops-54443 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.648 eng https://creativecommons.org/licenses/by/3.0/legalcode