A bounded arithmetic AID for Frege systems

DOI10.1016/S0168-0072(99)00041-XzbMath0959.03046arXivmath/9809205MaRDI QIDQ1977488

Toshiyasu Arai

Publication date: 2 May 2001

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/math/9809205

zbMATH Keywords

bounded arithmeticALOGTIMEFrege systemalogtime inductive definitions

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20)

Related Items

The NP Search Problems of Frege and Extended Frege Proofs ⋮ Function-algebraic characterizations of log and polylog parallel time ⋮ The equivalence of theories that characterize ALogTime ⋮ Expander Construction in VNC1 ⋮ Polynomal-size Frege proofs of Bollobás' theorem on the trace of sets ⋮ Quantified propositional calculus and a second-order theory for NC\(^{\text \textbf{1}}\) ⋮ Expander construction in \(\mathrm{VNC}^1\) ⋮ On theories of bounded arithmetic for \(\mathrm{NC}^1\) ⋮ Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II

Cites Work

• Propositional consistency proofs
• The graph of multiplication is equivalent to counting
• Bounded arithmetic for NC, ALogTIME, L and NL
• Polynomial size proofs of the propositional pigeonhole principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A bounded arithmetic AID for Frege systems