On the Complexity of Disjunction and Explicit Definability Properties in Some Intermediate Logics | SpringerLink
Skip to main content
Springer Nature Link
Log in

On the Complexity of Disjunction and Explicit Definability Properties in Some Intermediate Logics

  • Conference paper
  • First Online:
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2002)

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

Abstract

In this paper we provide a uniform framework, based on extraction calculi, where to study the complexity of the problem to decide the disjunction and the explicit definability properties for Intuitionistic Logic and some Superintuitionistic Logics. Unlike the previous approaches, our framework is independent of structural properties of the proof systems and it can be applied to Natural Deduction systems, Hilbert style systems and Gentzen sequent systems.

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. A. Avellone, M. Ferrari, and C. Fiorentini. A formal framework for synthesis and verification of logic programs. In K.-K. Lau, editor, Logic Based Program Synthesis and Transformation, 10th International Workshop, LOPSTR 2000, Selected Papers, volume 2042 of Lecture Notes in Computer Science, pages 1–17. Springer-Verlag, 2001.

    Google Scholar 

  2. S. Buss and G. Mints. The complexity of the disjunction and existential properties in intuitionistic logic. Annals of Pure and Applied Logic, 99(3):93–104, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  3. S. Buss and P. Pudlák. On the computational content of intuitionistic propositional proofs. Annals of Pure and Applied Logic, 109(1–2):49–64, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  4. M. Ferrari. Strongly Constructive Formal Systems. PhD thesis, Dipartimento di Scienze dell’Informazione, Universitá degli Studi di Milano, Italy, 1997. Available at http://homes.dsi.unimi.it/~ferram.

    Google Scholar 

  5. M. Ferrari and C. Fiorentini. A proof-theoretical analysis of semiconstructive intermediate theories. Studia Logica, to appear.

    Google Scholar 

  6. M. Ferrari, C. Fiorentini, and P. Miglioli. Goal oriented information extraction in uniformly constructive calculi. In Argentinian Workshop on Theoretical Computer Science (WAIT’99), pages 51–63. Sociedad Argentina de Informática e Investigación Operativa, 1999.

    Google Scholar 

  7. M. Ferrari, P. Miglioli, and M. Ornaghi. On uniformly constructive and semicon-structive formal systems. Logic Journal of the IGPL, to appear.

    Google Scholar 

  8. C. Fiorentini and P. Miglioli. A cut-free sequent calculus for the logic of constant domains with a limited amount of duplications. Logic Journal of the IGPL, 7(6):733–753, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  9. D.M. Gabbay. Semantical Investigations in Heyting’s Intuitionistic Logic. Reidel, Dordrecht, 1981.

    MATH  Google Scholar 

  10. S. Görnemann. A logic stronger than intuitionism. Journal of Symbolic Logic, 36:249–261, 1971.

    Article  MATH  MathSciNet  Google Scholar 

  11. G. Kreisel and H. Putnam. Eine Unableitbarkeitsbeweismethode für den intuition-istischen Aussagenkalkül. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 3:74–78, 1957.

    Article  MATH  MathSciNet  Google Scholar 

  12. P. Miglioli, U. Moscato, and M. Ornaghi. Constructive theories with abstract data types for program synthesis. In D.G. Skordev, editor, Mathematical Logic and its Applications, pages 293–302. Plenum Press, New York, 1987.

    Google Scholar 

  13. P. Miglioli, U. Moscato, and M. Ornaghi. Abstract parametric classes and abstract data types defined by classical and constructive logical methods. The Journal of Symbolic Computation, 18(1):41–81, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  14. H. Ono. Some results on the intermediate logics. Publications of the Research Institute for Mathematical Sciences, Kyoto University, 8:117–130, 1972.

    Article  Google Scholar 

  15. C.A. Smorynski. Applications of Kripke semantics. In A.S. Troelstra, editor, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics, pages 324–391. Springer-Verlag, 1973.

    Google Scholar 

  16. A.S. Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer-Verlag, 1973.

    Google Scholar 

  17. A.S. Troelstra and H. Schwichtenberg. Basic Proof Theory, volume 43 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Via Comelico 39, 20135, Milano, Italy

    Mauro Ferrari & Camillo Fiorentini

  2. CRII, Università dell’Insubria, Via Ravasi 2, 21100, Varese, Italy

    Guido Fiorino

Authors
  1. Mauro Ferrari
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Camillo Fiorentini
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Guido Fiorino
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Abteilung für Theoretische Informatik, Institut für Algebra und Diskrete Mathematik, Wiedner Hauptstr. 8-10, 1040, Wien, Austria

    Matthias Baaz

  2. Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, Manchester, M13, 9PL, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ferrari, M., Fiorentini, C., Fiorino, G. (2002). On the Complexity of Disjunction and Explicit Definability Properties in Some Intermediate Logics. In: Baaz, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2002. Lecture Notes in Computer Science(), vol 2514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36078-6_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-36078-6_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00010-5

  • Online ISBN: 978-3-540-36078-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation