A unification-theoretic method for investigating the k-provability problem

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


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



    Upload a copy of this work     Papers currently archived: 74,635

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

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

17 (#634,824)

6 months
1 (#419,510)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

The Undecidability of K-Provability.Samuel R. Buss - 1991 - Annals of Pure and Applied Logic 53 (1):75-102.
Algorithmic Structuring of Cut-Free Proofs.Matthias Baaz & Richard Zach - 1993 - In Egon Börger, Hans Kleine Büning, Gerhard Jäger, Simone Martini & Michael M. Richter (eds.), Computer Science Logic. CSL’92, San Miniato, Italy. Selected Papers. Berlin: Springer. pp. 29–42.
Bounded Arithmetic, Proof Complexity and Two Papers of Parikh.Samuel R. Buss - 1999 - Annals of Pure and Applied Logic 96 (1-3):43-55.

View all 7 citations / Add more citations

References found in this work

A Machine-Oriented Logic Based on the Resolution Principle.J. A. Robinson - 1966 - Journal of Symbolic Logic 31 (3):515-516.
A Simplified Formalization of Predicate Logic with Identity.Alfred Tarski - 1964 - Archive for Mathematical Logic 7 (1-2):61-79.
On Me Number of Steps in Proofs.Jan Krajíèek - 1989 - Annals of Pure and Applied Logic 41 (2):153-178.

View all 10 references / Add more references