Hostname: page-component-586b7cd67f-dlnhk Total loading time: 0 Render date: 2024-11-26T21:09:16.758Z Has data issue: false hasContentIssue false
  • English
  • Français

On the complexity of proof deskolemization

Published online by Cambridge University Press:  12 March 2014

Matthias Baaz ,
Stefan Hetzl  and
Daniel Weller
Matthias Baaz
Affiliation:
Institute of Discrete Mathematics and Geometry (E104), Vienna University of Technology, Wiedner Hauptstraße 8-10, 1040 Vienna, Austria, E-mail: [email protected]
Stefan Hetzl
Affiliation:
Laboratoire Preuves, Programmes et Systèmes (PPS), Université Paris Diderot – Paris 7, 175 Rue du Chevaleret, 75013 Paris, France, E-mail: [email protected]
Daniel Weller
Affiliation:
Institute of Computer Languages (E185), Vienna University of Technology, Favoritenstraβe 9, 1040 Vienna, Austria, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

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.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 77 , Issue 2 , June 2012 , pp. 669 - 686
Copyright
Copyright © Association for Symbolic Logic 2012

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Avigad, Jeremy, Eliminating definitions and Skolem functions in first-order logic, ACM Transactions on Computational Logic, vol. 4 (2003), no. 3, pp. 402–415.Google Scholar
[2] Baaz, Matthias and Leitsch, Alexander, Skolemization and proof complexity, Fundamenta Informaticae, vol. 20 (1994), no. 4, pp. 353–379.Google Scholar
[3] Baaz, Matthias and Leitsch, Alexander, Cut normalforms and proof complexity, Annals of Pure and Applied Logic, vol. 97 (1999), pp. 127–177.CrossRefGoogle Scholar
[4] Baaz, Matthias and Leitsch, Alexander, Cut-elimination and redundancy-elimination by resolution, Journal of Symbolic Computation, vol. 29 (2000), no. 2, pp. 149–176.Google Scholar
[5] Clote, Peter and Krajíček, Jan, Open problems, Arithmetic, proof theory and computational complexity (Clote, Peter and Krajíček, Jan, editors), Oxford University Press, 1993, pp. 1–19.Google Scholar
[6] Gentzen, Gerhard, Untersuchungen über das logische Schlieβen II, Mathematische Zeitschrift, vol. 39 (1935), no. 1, pp. 405–431.CrossRefGoogle Scholar
[7] Hähnle, Reiner and Schmitt, Peter H., The liberalized δ-rule in free variable semantic tableaux, Journal of Automated Reasoning, vol. 13 (1994), no. 2, pp. 211–221.Google Scholar
[8] Hilbert, David and Bernays, Paul, Grundlagen der Mathematik II, 2nd ed., Springer, 1970.Google Scholar
[9] Miller, Dale, A compact representation of proofs, Studia Logica, vol. 46 (1987), no. 4, pp. 347–370.Google Scholar
[10] Statman, Richard, Lower bounds on Herbrand's theorem, Proceedings of the American Mathematical Society, vol. 75 (1979), pp. 104–107.Google Scholar
[11] Troelstra, A. S. and Schwichtenberg, H., Basic proof theory, second ed., Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2000.Google Scholar