Journal article
A unification-theoretic method for investigating the k-provability problem
Abstract
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 (including individual axioms) and a finite number …
Authors
Farmer WM
Journal
Annals of Pure and Applied Logic, Vol. 51, No. 3, pp. 173–214
Publisher
Elsevier
Publication Date
March 1991
DOI
10.1016/0168-0072(91)90015-e
ISSN
0168-0072