On the complexity of proof deskolemization

, &
Journal of Symbolic Logic 77 (2):669-686 (2012)
  Copy   BIBTEX

Abstract

We consider the following problem: Given a proof of the Skolemization of a formula F, what is the length of the shortest proof of F? For the restriction of this question to cut-free proofs we prove corresponding exponential upper and lower bounds

Categories

Keywords

Reprint years

DOI

10.2178/jsl/1333566645

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,219

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 complexity of propositional proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
Propositional proof systems, the consistency of first order theories and the complexity of computations.Jan Krajíček & Pavel Pudlák - 1989 - Journal of Symbolic Logic 54 (3):1063-1079.
Complexity and sustainability.Jennifer Wells - 2013 - New York: Routledge.
.[author unknown] - unknown
Bounded arithmetic, propositional logic, and complexity theory.Jan Krajíček - 1995 - New York, NY, USA: Cambridge University Press.
Provability, complexity, grammars.Lev Dmitrievich Beklemishev - 1999 - Providence, RI: American Mathematical Society. Edited by Mati Reĭnovich Pentus & Nikolai Konstantinovich Vereshchagin.
Structured Pigeonhole Principle, Search Problems and Hard Tautologies.Jan Krajíček - 2005 - Journal of Symbolic Logic 70 (2):619 - 630.
Edgar Morin's paradigm of complexity and gödel's incompleteness theorem.Yi-Zhuang Chen - 2004 - World Futures 60 (5 & 6):421 – 431.
A new proof of the NP-completeness of visual match.Ronald A. Rensink - manuscript
Reasoning About Truth in First-Order Logic.Claes Strannegård, Fredrik Engström, Abdul Rahim Nizamani & Lance Rips - 2013 - Journal of Logic, Language and Information 22 (1):115-137.
Proof-theoretic modal pa-completeness I: A system-sequent metric.Paolo Gentilini - 1999 - Studia Logica 63 (1):27-48.
Synthetic analysis: How science combats complexity.Sunny Auyang - manuscript
Computational complexity and Godel's incompleteness theorem. McGraw-Hill - unknown

Analytics

Added to PP
2012-04-05

Downloads
65 (#240,360)

6 months
5 (#544,079)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Cut-Elimination: Syntax and Semantics.M. Baaz & A. Leitsch - 2014 - Studia Logica 102 (6):1217-1244.
A Simplified Proof of the Epsilon Theorems.Stefan Hetzl - forthcoming - Review of Symbolic Logic:1-16.
Induction and Skolemization in saturation theorem proving.Stefan Hetzl & Jannik Vierling - 2023 - Annals of Pure and Applied Logic 174 (1):103167.

Add more citations

References found in this work

A compact representation of proofs.Dale A. Miller - 1987 - Studia Logica 46 (4):347 - 370.
Cut normal forms and proof complexity.Matthias Baaz & Alexander Leitsch - 1999 - Annals of Pure and Applied Logic 97 (1-3):127-177.

Add more references