License: 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: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7689/
Go to the corresponding LIPIcs Volume Portal

Grädel, Erich ; Pago, Benedikt ; Pakusa, Wied

The Model-Theoretic Expressiveness of Propositional Proof Systems

pdf-format:
LIPIcs-CSL-2017-27.pdf (0.5 MB)

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
Collection: 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Issue Date: 2017
Date of publication: 16.08.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI