Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 1997: Automated Deduction—CADE-14 pp 116–130Cite as

Some pitfalls of LK-to-LJ translations and how to avoid them

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1249))

Abstract

In this paper, we investigate translations from a classical cut-free sequent calculus LK into an intuitionistic cut-free sequent calculus LJ. Translations known from the literature rest on permutations of inferences in classical proofs. We show that, for some classes of first-order formulae, all minimal LJ-proofs are non-elementary but there exist short LK-proofs of the same formula. Similar results are obtained even if some fragments of intuitionistic first-order logic are considered. The size of the corresponding minimal search spaces for LK and LJ are also non-elementarily related. We show that we can overcome these difficulties by extending LJ with an analytic cut rule.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Eder. Relative Complexities of First Order Calculi. Vieweg, Braunschweig, 1992.

    Book  Google Scholar 

  2. U. Egly. On Different Structure-preserving Translations to Normal Form. J. Symbolic Computation, 22:121–142, 1996.

    Article  MathSciNet  Google Scholar 

  3. U. Egly. On Definitional Translations to Normal Form for Intuitionistic Logic. Fundamenta Informaticae, 29(1,2):165–201, 1997.

    MathSciNet  MATH  Google Scholar 

  4. G. Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1935. English translation in [13].

    Article  MathSciNet  Google Scholar 

  5. G. Mints. Proof Theory in the USSR 1925–1969. J. Symbolic Logic, 56(2):385–424, 1991.

    Article  MathSciNet  Google Scholar 

  6. G. Mints. Resolution Strategies for the Intuitionistic Logic. In B. Mayoh, E. Tyugu, and J. Penyam, editors, Constraint Programming, Nato ASI Series, pages 289–311. Springer Verlag, 1994.

    Google Scholar 

  7. V. P. Orevkov. On Glivenko Sequent Classes. In V. P. Orevkov, editor, The calculi of Symbolic Logic I, volume 98, pages 147–173. Steklov Institute of Mathematics, 1971.

    Google Scholar 

  8. V. P. Orevkov. Lower Bounds for Increasing Complexity of Derivations after Cut Elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im V. A. Steklova AN SSSR, 88:137–161, 1979. English translation in J. Soviet Mathematics, 2337–2350, 1982.

    MATH  Google Scholar 

  9. D. A. Plaisted and S. Greenbaum. A Structure-Preserving Clause Form Translation. J. Symbolic Computation, 2:293–304, 1986.

    Article  MathSciNet  Google Scholar 

  10. D. Pym, E. Ritter, and L. Wallen. On the Intuitionistic Force of Classical Search. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Theorem Proving with Analytic Tableaux and Related Methods, pages 295–311. Springer Verlag, 1996.

    Google Scholar 

  11. D. Pym, E. Ritter, and L. Wallen. Proof-Terms for Classical and Intuitionistic Resolution. In M.A. McRobbie and J. K. Slaney, editors, Proceedings of the Conference on Automated Deduction, pages 17–31. Springer Verlag, 1996.

    Google Scholar 

  12. R. Statman. Intuitionistic Propositional Logic is Polynomial-Space Complete. J. Theoretical Computer Science, 9:67–72, 1979.

    Article  MathSciNet  Google Scholar 

  13. M. E. Szabo, editor. The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, 1969.

    Google Scholar 

  14. G. Takeuti. Proof Theory, volume 81 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, 1975.

    Google Scholar 

  15. G. S. Tseitin. On the Complexity of Derivation in Propositional Calculus. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning, pages 466–483. Springer Verlag, 1983.

    Google Scholar 

  16. A. Voronkov. Theorem Proving in Non-standard Logics Based on the Inverse Method. In D. Kapur, editor, Proceedings of the Conference on Automated Deduction, pages 648–662. Springer Verlag, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Abt. Wissensbasierte Systeme 184/3, TU Wien, Treitlstraße 3, A-1040, Wien, Austria

    Uwe Egly

Authors
  1. Uwe Egly
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

William McCune

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Egly, U. (1997). Some pitfalls of LK-to-LJ translations and how to avoid them. In: McCune, W. (eds) Automated Deduction—CADE-14. CADE 1997. Lecture Notes in Computer Science, vol 1249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63104-6_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-63104-6_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63104-0

  • Online ISBN: 978-3-540-69140-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation