文章基本信息

标题：The Model-Theoretic Expressiveness of Propositional Proof Systems
本地全文：下载
作者：Grädel, Erich ; Benedikt Pago ; Wied Pakusa 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：82
页码：27:1-27:18
DOI：10.4230/LIPIcs.CSL.2017.27
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Propositional proof systems; fixed-point logics; resolution; polynomial calculus; generalized quantifiers