Bounds for proof-search and speed-up in the predicate calculus

Annals of Mathematical Logic 15 (3):225 (1978)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.1016/0003-4843(78)90011-6

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,283

External links

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

Through your library

My notes

Similar books and articles

The cost of a cycle is a square.A. Carbone - 2002 - Journal of Symbolic Logic 67 (1):35-60.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Upper Bounds for Proof-Search in a Sequent Calculus for Relational Equations.Wolfgang Schönfeld - 1982 - Mathematical Logic Quarterly 28 (14-18):239-246.
Complexity of Null- and Positivstellensatz proofs.Dima Grigoriev & Nicolai Vorobjov - 2001 - Annals of Pure and Applied Logic 113 (1-3):153-160.
Inferentializing consequence.Jaroslav Peregrin - unknown
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Proof complexity of propositional default logic.Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas & Heribert Vollmer - 2011 - Archive for Mathematical Logic 50 (7-8):727-742.
A Deterministic Terminating Sequent Calculus For Gödel-dummett Logic.R. Dyckhoff - 1999 - Logic Journal of the IGPL 7 (3):319-326.
Intuitionistic Logic Freed of All Metarules.Giovanna Corsi & Gabriele Tassi - 2007 - Journal of Symbolic Logic 72 (4):1204 - 1218.
Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
The complexity of the disjunction and existential properties in intuitionistic logic.Sam Buss & Grigori Mints - 1999 - Annals of Pure and Applied Logic 99 (1-3):93-104.
Classical Non-Associative Lambek Calculus.Philippe De Groote & François Lamarche - 2002 - Studia Logica 71 (3):355 - 388.
Interpolation theorems, lower Bounds for proof systems, and independence results for bounded arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
A semantical proof of De Jongh's theorem.Jaap van Oosten - 1991 - Archive for Mathematical Logic 31 (2):105-114.
Kleene S. C.. Permutability of inferences in Gentzen's calculi LK and LJ. Two papers on the predicate calculus, by Kleene S. C. , lithographed, Providence 1952, pp. 1–26.Kleene S. C.. Finite axiomatizability of theories in the predicate calculus using additional predicate symbols. Two papers on the predicate calculus, by Kleene S. C. , lithographed, Providence 1952, pp. 27–66.Kleene S. C.. Bibliography. Two papers on the predicate calculus, by Kleene S. C. , lithographed, Providence 1952, pp. 67–68.Craig William. On axiomatizability within a system. [REVIEW]Robert McNaughton - 1954 - Journal of Symbolic Logic 19 (1):62-63.

Analytics

Added to PP
2014-01-17

Downloads
22 (#713,252)

6 months
8 (#370,373)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Cuts, consistency statements and interpretations.Pavel Pudlák - 1985 - Journal of Symbolic Logic 50 (2):423-441.
A curious inference.George Boolos - 1987 - Journal of Philosophical Logic 16 (1):1 - 12.
On me number of steps in proofs.Jan Krajíèek - 1989 - Annals of Pure and Applied Logic 41 (2):153-178.

View all 26 citations / Add more citations

References found in this work

The collected papers of Gerhard Gentzen.Gerhard Gentzen - 1969 - Amsterdam,: North-Holland Pub. Co.. Edited by M. E. Szabo.
The Calculi of Lambda-conversion.Alonzo Church - 1985 - Princeton, NJ, USA: Princeton University Press.
Ideas and Results in Proof Theory.Dag Prawitz & J. E. Fenstad - 1971 - Journal of Symbolic Logic 40 (2):232-234.
A Machine-Oriented Logic based on the Resolution Principle.J. A. Robinson - 1966 - Journal of Symbolic Logic 31 (3):515-516.
Intensional interpretations of functionals of finite type I.W. W. Tait - 1967 - Journal of Symbolic Logic 32 (2):198-212.

View all 10 references / Add more references