Skip to main content
SpringerLink
Log in

Focused Natural Deduction

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6397))

Abstract

Natural deduction for intuitionistic linear logic is known to be full of non-deterministic choices. In order to control these choices, we combine ideas from intercalation and focusing to arrive at the calculus of focused natural deduction. The calculus is shown to be sound and complete with respect to first-order intuitionistic linear natural deduction and the backward linear focusing calculus.

This work was in part supported by NABITT grant 2106-07-0019 of the Danish Strategic Research Council.

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

Access this chapter

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andreoli, J.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2(3), 297 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  2. Chaudhuri, K.: Focusing strategies in the sequent calculus of synthetic connectives. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 467–481. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Chaudhuri, K., Miller, D., Saurin, A.: Canonical sequent proofs via multi-focusing. In: Fifth International Conference on Theoretical Computer Science, vol. 273, pp. 383–396. Springer, Heidelberg (2008)

    Google Scholar 

  4. Chaudhuri, K., Pfenning, F., Price, G.: A logical characterization of forward and backward chaining in the inverse method. Journal of Automated Reasoning 40(2), 133–177 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  5. Krishnaswami, N.R.: Focusing on pattern matching. In: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 366–378. ACM, New York (2009)

    Google Scholar 

  6. Licata, D.R., Zeilberger, N., Harper, R.: Focusing on binding and computation. In: LICS, pp. 241–252. IEEE Computer Society, Los Alamitos (2008)

    Google Scholar 

  7. McLaughlin, S., Pfenning, F.: Efficient intuitionistic theorem proving with the polarized inverse method. In: Proceedings of the 22nd International Conference on Automated Deduction, p. 244. Springer, Heidelberg (2009)

    Google Scholar 

  8. Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Logic 51(1-2), 125–157 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  9. Prawitz, D.: Natural Deduction. Almquist & Wiksell, Stockholm (1965)

    Google Scholar 

  10. Sieg, W., Byrnes, J.: Normal natural deduction proofs (in classical logic). Studia Logica 60(1), 67–106 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  11. Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework: The propositional fragment. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 355–377. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  12. Zeilberger, N.: Focusing and higher-order abstract syntax. In: Necula, G.C., Wadler, P. (eds.) POPL, pp. 359–369. ACM, New York (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IT University of Copenhagen, Denmark

    Taus Brock-Nannestad & Carsten Schürmann

Authors
  1. Taus Brock-Nannestad
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Carsten Schürmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Computersprachen 185.2, Theory and Logic Group, TU Wien, Favoritenstraße 9-11, A-1040, Vienna, Austria

    Christian G. Fermüller

  2. School of Computer Science, University of Manchester, Oxford Road, Kilburn Building, M13 9PL, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brock-Nannestad, T., Schürmann, C. (2010). Focused Natural Deduction. In: Fermüller, C.G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science, vol 6397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16242-8_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16242-8_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16241-1

  • Online ISBN: 978-3-642-16242-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation