A second-order system for polytime reasoning based on Grädel's theorem.
type: Item
instance of: scholarly article
title: A second-order system for polytime reasoning based on Grädel's theorem.
zbMATH Open document ID: 1036.03042
DOI: 10.1016/S0168-0072(03)00056-3
author: Stephen Cook
author: Antonina Kolokolova
published in: Annals of Pure and Applied Logic
publication date: 2003-11-25T00:00:00Z
review text: The authors introduce a second-order system, \(V_{1}\)-Horn, of bounded arithmetic formalizing polynomial-time reasoning based on Grädel's second-order Horn characterization of P. It is proved that this system is equivalent to QPV and Zambella's P-def. It is also shown that \(V_{1}\)-Horn is finitely axiomatizable and that the class of \(\forall \Sigma^{b}_{1}\) consequences of \(S^{1}_{2}\) is finitely axiomatizable as well. This answers an open question.
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 68Q19
Mathematics Subject Classification ID: 68Q15
zbMATH DE Number: 2009287
zbMATH Keywords: Bounded arithmetic
zbMATH Keywords: Polynomial time
zbMATH Keywords: Second-order system
zbMATH Keywords: Descriptive complexity
reviewed by: Roman Murawski
MaRDI profile type: Publication
cites work: On uniformity within \(NC^ 1\)
cites work: Q3794177
cites work: Q3476809
cites work: Relating the bounded arithmetic and polynomial time hierarchies
cites work: Q4133141
cites work: Q4375787
cites work: Functional interpretations of feasibly constructive arithmetic
cites work: Q4058132
cites work: Q4035693
cites work: Capturing complexity classes by fragments of second-order logic
cites work: Q4843270
cites work: Relational queries computable in polynomial time
cites work: Q4227581
cites work: Q4856172
cites work: Bounded arithmetic and the polynomial hierarchy
cites work: Descriptive characterizations of computational complexity
cites work: Q3140640
cites work: Q4219291
cites work: The polynomial-time hierarchy
cites work: Q3140644
cites work: Notes on polynomially bounded arithmetic
description: scientific article; zbMATH DE number 2009287