[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Normal Natural Deduction Proofs (in Non-classical Logics)

  • Chapter
Mechanizing Mathematical Reasoning

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

Abstract

We provide a theoretical framework that allows the direct search for natural deduction proofs in some non-classical logics, namely, intuitionistic sentential and predicate logic, but also in the modal logic S4. The framework uses so-called intercalation calculi to build up broad search spaces from which normal proofs can be extracted, if a proof exists at all. This claim is supported by completeness proofs establishing in a purely semantic way normal form theorems for the above logics. Logical restrictions on the search spaces are briefly discussed in the last section together with some heuristics for structuring a more efficient search. Our paper is a companion piece to [15], where classical logic was treated.

This paper is dedicated to Jörg Siekmann, pragmatic visionary.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Avron, A., Honsell, F., Miculan, M., Paravano, C.: Encoding Modal Logics in Logical Frameworks. Studia Logica 60(1), 161–208 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  2. Basin, D., Matthews, S., Viganò, L.: Natural Deduction for Non-Classical Logics. Studia Logica 60(1), 119–160 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  3. Byrnes, J.: Proof Search and Normal Forms for Natural Deductions. PhD thesis, Carnegie Mellon University (1999)

    Google Scholar 

  4. Cittadini, S.: Intercalation calculus for intuitionistic propositional logic. Technical Report PHIL-29, Philosophy, Methodology, and Logic, Carnegie Mellon University (1992)

    Google Scholar 

  5. Cittadini, S.: Deduzione Naturale e Ricerca Automatica di Dimostrazioni in varie logiche: il Calcolo delle Intercalazioni. In: Cellucci, C., Di Maio, M. C., Roncaglia, G. (eds.): Atti del Congresso Logica e filosofia della scienza: problemi e prospettive, Lucca, Pisa, gennaio 7–10, pp. 583–591. Edizioni ETS (1993)

    Google Scholar 

  6. van Dalen, D.: Logic and Structure, 2nd edn. Springer, Heidelberg (1989)

    MATH  Google Scholar 

  7. Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. The Journal of Symbolic Logic 57(3), 795–807 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  8. Fitting, M.: Intuitionistic Logic Model Theory and Forcing. North-Holland Publishing Company, Amsterdam (1969)

    MATH  Google Scholar 

  9. Fitting, M.: Proof Methods for Modal and Intuitionistic Logic. D. Reidel Publishing Company, Dordrecht (1983)

    Google Scholar 

  10. Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1989)

    MATH  Google Scholar 

  11. Harrop, R.: Concerning formulas of the types A → B ∨ C, A → (Ex)B(x) in intuitionistic formal systems. The Journal of Symbolic Logic 25(1), 27–32 (1960)

    Article  MATH  MathSciNet  Google Scholar 

  12. Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiskell, Stockholm (1965)

    MATH  Google Scholar 

  13. Shankar, N.: Proof search in the intuitionistic sequent calculus. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 522–536. Springer, Heidelberg (1992)

    Google Scholar 

  14. Sieg, W.: Mechanisms and Search: Aspects of Proof Theory. AILA Preprint 19, Associazione Italiana di Logica e sue Applicazioni, Padova (1992)

    Google Scholar 

  15. Sieg, W., Byrnes, J.: Normal Natural Deduction Proofs (in classical logic). Studia Logica 60(1), 67–106 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  16. Sieg, W., Cittadini, S.: Normal Natural Deduction Proofs (in non-classical logics). Rapporto Matematico n. 351, Dipartimento di Matematica, Università di Siena (1998)

    Google Scholar 

  17. Sieg, W., Scheines, R.: Searching for proofs (in sentential logic). In: Burkholder, L. (ed.) Philosophy and the Computer, pp. 137–159. Westview Press, Boulder (1992)

    Google Scholar 

  18. Statman, R.: Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science 9(1), 67–72 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  19. Tennant, N.: Autologic. Edinburgh University Press, Edinburgh (1992)

    Google Scholar 

  20. Wallen, L.A.: Automated Proof Search in Non-Classical Logics. MIT Press, Cambridge (1990)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Philosophy, Carnegie Mellon University, 5000 Forbes Ave., Pittsburgh, PA, 15213, USA

    Wilfried Sieg

  2. Dipartimento di Matematica e Scienze Informatiche “R. Magari”, Università di Siena, Via del Capitano 15, I-53100, Siena, Italy

    Saverio Cittadini

Authors
  1. Wilfried Sieg
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Saverio Cittadini
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DFKI, Stuhlsatzenhausweg 3, D-66123, Saarbrücken, Germany

    Dieter Hutter

  2. German Research Center for Artificial Intelligence, DFKI GmbH,  

    Werner Stephan

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Sieg, W., Cittadini, S. (2005). Normal Natural Deduction Proofs (in Non-classical Logics). In: Hutter, D., Stephan, W. (eds) Mechanizing Mathematical Reasoning. Lecture Notes in Computer Science(), vol 2605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32254-2_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-32254-2_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-25051-7

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation