Focusing the Inverse Method for Linear Logic

  • Kaustuv Chaudhuri
  • Frank Pfenning
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


Focusing is traditionally seen as a means of reducing inessential non-determinism in backward-reasoning strategies such as uniform proof-search or tableaux systems. In this paper we construct a form of focused derivations for propositional linear logic that is appropriate for forward reasoning in the inverse method. We show that the focused inverse method conservatively generalizes the classical hyperresolution strategy for Horn-theories, and demonstrate through a practical implementation that the focused inverse method is considerably faster than the non-focused version.


Inverse Method Intuitionistic Logic Linear Logic Horn Clause Sequent Calculus 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andreoli, J.M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2, 297–347 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Andreoli, J.M.: Focussing and proof construction. Annals of Pure and Applied Logic 107, 131–163 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Howe, J.M.: Proof Search Issues in Some Non-Classical Logics. PhD thesis, University of St. Andrews (1998)Google Scholar
  4. 4.
    Girard, J.Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Barber, A.: Dual Intuitionistic Linear Logic. Technical Report ECS-LFCS-96-347, University of Edinburgh (1996)Google Scholar
  6. 6.
    Chang, B.Y.E., Chaudhuri, K., Pfenning, F.: A judgmental analysis of linear logic. Technical Report CMU-CS-03-131R, Carnegie Mellon University (2003)Google Scholar
  7. 7.
    Cervesato, I., Pfenning, F., Walker, D., Watkins, K.: A concurrent logical framework I & II. Technical Report CMU-CS-02-101 and 102, Department of Computer Science, Carnegie Mellon University (2002) (revised May 2003) Google Scholar
  8. 8.
    Degtyarev, A., Voronkov, A.: The Inverse Method. In: Handbook of Automated Reasoning, pp. 179–272. MIT Press, Cambridge (2001)CrossRefGoogle Scholar
  9. 9.
    Chaudhuri, K., Pfenning, F.: A focusing inverse method theorem prover for first-order linear logic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 69–83. Springer, Heidelberg (2005) (to appear)CrossRefGoogle Scholar
  10. 10.
    Tammet, T.: Resolution, inverse method and the sequent calculus. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1997. LNCS, vol. 1289, pp. 65–83. Springer, Heidelberg (1997)Google Scholar
  11. 11.
    Mints, G.: Resolution calculus for the first order linear logic. Journal of Logic. Language and Information 2, 59–83 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for linear logic proof search. Theoretical Computer Science 232, 133–163 (2000); Special issue on Proof Search in Type-Theoretic Languages, D. Galmiche and D. Pym, editorszbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Harland, J., Pym, D.J.: Resource-distribution via boolean constraints. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 222–236. Springer, Heidelberg (1997)Google Scholar
  14. 14.
    Girard, J.Y.: Locus solum: from the rules of logic to the logic of rules. Mathematical Structures in Computer Science 11, 301–506 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Chaudhuri, K., Pfenning, F.: Focusing the inverse method for linear logic. Technical Report CMU-CS-05-106, Carnegie Mellon University (2005)Google Scholar
  16. 16.
    Lincoln, P., Mitchell, J.C., Scedrov, A., Shankar, N.: Decision problems for propositional linear logic. Annals of Pure and Applied Logic 56, 239–311 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 795–807 (1992)Google Scholar
  18. 18.
    Bozzano, M., Delzanno, G., Martelli, M.: Model checking linear logic specifications. TPLP 4, 573–619 (2004)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Kaustuv Chaudhuri
    • 1
  • Frank Pfenning
    • 1
  1. 1.Department of Computer ScienceCarnegie Mellon University 

Personalised recommendations