Binding Forms in First-Order Logic. Mogavero, F. & 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]](https://bibbase.org/img/filetypes/link.svg "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_paper = "{https://drops.dagstuhl.de/opus/volltexte/2015/5444/}",
}
Downloads: 0
{"_id":"9mejMnEvFL9MDPWjS","bibbaseid":"mogavero-perelli-bindingformsinfirstorderlogic-2015","authorIDs":["27AAjNDH3eGyX3kAG","5e5fa91819c3fade010000c4","5e610d2131c7d3de0100025f","5e65076e9eed46de0100004a","5e6aaadaf216f6de01000129","62BzuGuQtetH6F3cf","73Rh8BSJgqcii5cD3","7aQ2zeLMoyj6CHpBu","8QYqvnERKkScTLpXt","939RNK33yrPF4hHck","9QZmYec3ABqZqB9ed","9R3rFYeegwqLCtFQ7","9y2sud2AwvG4Tfdrm","Am2578MapgxQHtFf4","AqbTCnnCr8sLjTmdv","Ax9iPx6jhgbzjgAsq","C4ESoeg7imBRZM8Wr","DCAwSuxCjnszReHdG","FSKJKgCA2iK6ike3h","G2yqkXwcYagjLqEat","Gj4YRNsBu7wtb4vXY","HcptFeK4rg5nYWiFa","HfSGhTtE2kahBfnm8","HuLSgG4PJuPLGpoMZ","JYgujoQ6Yr9gf5vNm","JqvuFYYZoqT3y5hMJ","JsDz5ZfswX5PojvGF","L9SALwZHK7h4cnemm","M8ugQbFqc7J2SZZkb","MFXN3rfY97dER4uaF","MZzQLYonZyupKJJTW","Mj26qo7ejPRPakyYe","P7Rrykvikzyq7PH8F","SJHQwhWmEBwe2BkD3","TXDn8che9rTzjmrA5","W7Y9wsvLY9xYhYm7h","WrDgnRcn4BB4Pa2dL","XFeNGvuLa7vugKn8p","b932A83vqaao9vcAc","g5b8qR96euxXJQuwo","kWEPDQzitMRJ7Zfhd","kZpNRST28n9ZjkEjH","n5xPfBLskvCDRBk9A","pJotjgR9RGRzfaYDG","phZeTXoR5izbbuka9","qNnrc72DLfCFyCBuC","qWWZLuDKbdrQDYuXX","uiiEzMohLiEYpDQLf","uj2FY3LBd7XX9c4LZ","wGdyWcm2XzfxzJTEK","xPnSDmeSsJoXtiWXX","xWfKBfkZej5XRKp8G"],"author_short":["Mogavero, F.","Perelli, G."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Fabio"],"propositions":[],"lastnames":["Mogavero"],"suffixes":[]},{"firstnames":["Giuseppe"],"propositions":[],"lastnames":["Perelli"],"suffixes":[]}],"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_paper":"https://drops.dagstuhl.de/opus/volltexte/2015/5444/","bibtex":"@inproceedings\n\t{\n\tC-MP15b,\n\tauthor\t\t\t\t=\t{Fabio Mogavero and Giuseppe Perelli},\n\ttitle\t\t\t\t\t=\t{Binding Forms in First-Order Logic.},\n\tabstract\t\t\t=\t{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.},\n\tbooktitle\t\t\t=\t{24th {EACSL} Annual Conference on Computer Science Logic, {CSL} 2015, September 7-10, 2015, Berlin, Germany},\n\tpages\t\t\t\t\t=\t\"{648--665}\",\n\tyear\t\t\t\t\t=\t\"{2015}\",\n\turl_paper\t\t\t=\t\"{https://drops.dagstuhl.de/opus/volltexte/2015/5444/}\",\n\t}\n\t\n","author_short":["Mogavero, F.","Perelli, G."],"key":"C-MP15b","id":"C-MP15b","bibbaseid":"mogavero-perelli-bindingformsinfirstorderlogic-2015","role":"author","urls":{" paper":"https://drops.dagstuhl.de/opus/volltexte/2015/5444/"},"metadata":{"authorlinks":{"perelli, g":"https://giuseppeperelli.github.io/oldsite/"}}},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/giuseppeperelli/giuseppeperelli.github.io/master/Publications.bib","creationDate":"2020-02-29T21:07:14.954Z","downloads":0,"keywords":[],"search_terms":["binding","forms","first","order","logic","mogavero","perelli"],"title":"Binding Forms in First-Order Logic.","year":2015,"dataSources":["Hsp4YyumSZ65qLatJ","kSN38gKTSZ2dArL6M","P3TQkzzbYMHFrjwn4"]}