No Cover Image

Journal article 550 views

Uniform Proof Complexity / A Beckmann; Arnold Beckmann

Journal of Logic and Computation, Volume: 15, Issue: 4, Pages: 433 - 446

Swansea University Author: Arnold, Beckmann

Full text not available from this repository: check for access using links below.

Check full text

DOI (Published version): 10.1093/logcom/exi035

Abstract

We define the notion of the uniform reduct of a propositional proof system as the set of those bounded formulas in the language of Peano Arithmetic which have polynomial size proofs under the Paris-Wilkie-translation. With respect to the arithmetic complexity of uniform reducts, we show that uniform...

Full description

Published in: Journal of Logic and Computation
ISSN: 0955-792X 1465-363X
Published: 2005
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa1702
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: We define the notion of the uniform reduct of a propositional proof system as the set of those bounded formulas in the language of Peano Arithmetic which have polynomial size proofs under the Paris-Wilkie-translation. With respect to the arithmetic complexity of uniform reducts, we show that uniform reducts are \Pi^0_1-hard and obviously in \Sigma^0_2. We also show under certain regularity conditions that each uniform reduct is closed under bounded generalisation; that in the case the language includes a symbol for exponentiation, a uniform reduct is closed under modus ponens if and only if it already contains all true bounded formulas; and that each uniform reduct contains all true \Pi^b_1(\alpha)-formulas.
College: College of Science
Issue: 4
Start Page: 433
End Page: 446