Binding Forms in First-Order Logic. Mogavero, F. and Perelli, G. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, pages 648–665, 2015.
Binding Forms in First-Order Logic. [link]Paper  abstract   bibtex   
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
	{
	C-MP15b,
	author				=	{Fabio Mogavero and Giuseppe Perelli},
	title					=	{Binding Forms in First-Order Logic.},
	abstract			=	{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.},
	booktitle			=	{24th {EACSL} Annual Conference on Computer Science Logic, {CSL} 2015, September 7-10, 2015, Berlin, Germany},
	pages					=	"{648--665}",
	year					=	"{2015}",
	url						=	"{https://drops.dagstuhl.de/opus/volltexte/2015/5444/}",
	}
Downloads: 0