文章基本信息

标题：Binding Forms in First-Order Logic
本地全文：下载
作者：Fabio Mogavero ; Giuseppe Perelli
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：41
页码：648-665
DOI：10.4230/LIPIcs.CSL.2015.648
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：First-Order Logic; Decidable Fragments; Satisfiability; Model Checking