Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2017.27
URN: urn:nbn:de:0030-drops-76897
URL: https://drops.dagstuhl.de/opus/volltexte/2017/7689/
Grädel, Erich ; Pago, Benedikt ; Pakusa, Wied
The Model-Theoretic Expressiveness of Propositional Proof Systems
| pdf-format: |
|
Abstract
We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory.Specifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded width resolution, and the polynomial calculus of bounded degree, can be characterised in a precise sense by variants of fixed-point logics that are of fundamental importance in descriptive complexity theory.
Our main results are that Horn resolution has the same expressive power as least fixed-point logic, that bounded width resolution captures existential least fixed-point logic, and that the (monomial restriction of the) polynomial calculus of bounded degree solves precisely the problems definable in fixed-point logic with counting.
BibTeX - Entry
@InProceedings{grdel_et_al:LIPIcs:2017:7689,
author = {Erich Gr{\"a}del and Benedikt Pago and Wied Pakusa},
title = {{The Model-Theoretic Expressiveness of Propositional Proof Systems}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {27:1--27:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Valentin Goranko and Mads Dam},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7689},
URN = {urn:nbn:de:0030-drops-76897},
doi = {10.4230/LIPIcs.CSL.2017.27},
annote = {Keywords: Propositional proof systems, fixed-point logics, resolution, polynomial calculus, generalized quantifiers}
}
| Keywords: | Propositional proof systems, fixed-point logics, resolution, polynomial calculus, generalized quantifiers | |
| Seminar: | 26th EACSL Annual Conference on Computer Science Logic (CSL 2017) | |
| Issue date: | 2017 | |
| Date of publication: | 16.08.2017 |
