Annals of Pure and Applied Logic 51 (3):173-214 (1991)

The k-provability for an axiomatic system A is to determine, given an integer k 1 and a formula in the language of A, whether or not there is a proof of in A containing at most k lines. In this paper we develop a unification-theoretic method for investigating the k-provability problem for Parikh systems, which are first-order axiomatic systems that contain a finite number of axiom schemata and a finite number of rules of inference. We show that the k-provability problem for a Parikh system reduces to a unification problem that is essentially the unification problem for second-order terms. By solving various subproblems of this unification problem , we solve the k- probability problem for a variety of Parikh systems, including several formulations of Peano arithmetic. Our method for investigating the k-provability problem employs algorithms that compute and characterize unifiers. We give some examples of how these algorithms can be used to solve complexity problems other than the k-provability problem
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/0168-0072(91)90015-e
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 59,687
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

A Machine-Oriented Logic Based on the Resolution Principle.J. A. Robinson - 1966 - Journal of Symbolic Logic 31 (3):515-516.
On Me Number of Steps in Proofs.Jan Krajíèek - 1989 - Annals of Pure and Applied Logic 41 (2):153-178.
Sets of Theorems with Short Proofs.Daniel Richardson - 1974 - Journal of Symbolic Logic 39 (2):235-242.

View all 10 references / Add more references

Citations of this work BETA

The Undecidability of K-Provability.Samuel R. Buss - 1991 - Annals of Pure and Applied Logic 53 (1):75-102.
Bounded Arithmetic, Proof Complexity and Two Papers of Parikh.Samuel R. Buss - 1999 - Annals of Pure and Applied Logic 96 (1-3):43-55.
A Note on the Length of Proofs.Tsuyoshi Yukami - 1994 - Annals of the Japan Association for Philosophy of Science 8 (4):203-209.

View all 6 citations / Add more citations

Similar books and articles

Degrees of Relative Provability.Mingzhong Cai - 2012 - Notre Dame Journal of Formal Logic 53 (4):479-489.
The Undecidability of the Second Order Predicate Unification Problem.Gilles Amiot - 1990 - Archive for Mathematical Logic 30 (3):193-199.
The Decision Problem of Provability Logic with Only One Atom.Vítězslav Švejdar - 2003 - Archive for Mathematical Logic 42 (8):763-768.
Unification and Explanation.Erik Weber & Maarten Van Dyck - 2002 - Synthese 131 (1):145 - 154.
Best Unifiers in Transitive Modal Logics.Vladimir V. Rybakov - 2011 - Studia Logica 99 (1-3):321-336.
Saturated Models of Universal Theories.Jeremy Avigad - 2002 - Annals of Pure and Applied Logic 118 (3):219-234.
Highly Constrained Unification Grammars.Daniel Feinstein & Shuly Wintner - 2008 - Journal of Logic, Language and Information 17 (3):345-381.
Fibred Semantics for Feature-Based Grammar Logic.Jochen Dörre, Esther König & Dov Gabbay - 1996 - Journal of Logic, Language and Information 5 (3-4):387-422.


Added to PP index

Total views
16 ( #629,083 of 2,432,280 )

Recent downloads (6 months)
1 ( #466,747 of 2,432,280 )

How can I increase my downloads?


My notes