Skip to main content
SpringerLink
Log in

linTAP : A Tableau Prover for Linear Logic

  • Conference paper
  • First Online:
Book cover Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 1999)

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

Abstract

linTAP is a tableau prover for the multiplicative and exponential fragment \( \mathcal{M}?\mathcal{L}\mathcal{L} \) of Girards linear logic. It proves the validity of a given formula by constructing an analytic tableau and ensures the linear validity using prefix unification. We present the tableau calculus used by linTAP, an algorithm for prefix unification in linear logic, the linTAP implementation, and some experimental results obtained with linTAP.

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 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

    Article  MATH  MathSciNet  Google Scholar 

  2. B. Beckert, J. Posegga. lean TAP: Lean Tableau-Based Theorem Proving. 12 th Conference on Automated Deduction, LNAI 814, pp. 793–797. Springer, 1994.

    Google Scholar 

  3. B. Beckert, J. Posegga. leanTAP: Lean Tableau-Based Deduction. Journal of Automated Reasoning, 15(3), pp. 339–358, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  4. B. Beckert, R. Goré. Free Variable Tableaux for Propositional Modal Logics. Proc. 6 th TABLEAUX Conference, LNAI 1227, pp. 91–106, Springer 1997.

    Google Scholar 

  5. W. Bibel. Let’s plan it deductively!. In IJCAI-97, Morgan Kaufmann, 1997.

    Google Scholar 

  6. I. Cervesato, J.S. Hodas, F. Pfenning. Efficient resource management for linear logic proof search. In Extensions of Logic Programming, LNAI 1050, pages 67–81. Springer, 1996.

    Google Scholar 

  7. M. Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1996.

    Google Scholar 

  8. B. Fronhöfer. The action-as-implication paradigm. CS Press, 1996.

    Google Scholar 

  9. D. Galmiche. Connection methods in linear logic fragments and proof nets. Technical report, CADE-13 workshop on proof search in type-theoretic languages, 1996.

    Google Scholar 

  10. D. Galmiche & G. Perrier. On proof normalization in linear logic. TCS, 135:67–110, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  11. V. Gehlot and C. Gunter. Normal process representatives. Sixth Annual Symposium on Logic in Computer Science, pages 200–207, 1991.

    Google Scholar 

  12. J.-Y. Girard. Linear logic. TCS, 50:1–102, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  13. J. Harland and D. Pym. Resource-Distribution via Boolean Constraints. 14 th Conference on Automated Deduction, LNCS 1249, pp. 222–236. Springer, 1997.

    Google Scholar 

  14. J.S. Hodas & D. Miller. Logic programming in a fragment of linear logic. Journal of Information and Computation, 110(2):327–365, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  15. C. Kreitz, H. Mantel, J. Otten, S. Schmitt. Connection-Based Proof Construction in Linear Logic. 14 th Conference on Automated Deduction, LNCS 1249, pp. 207–221. Springer, 1997.

    Google Scholar 

  16. P. Lincoln and T. Winkler. Constant-only multiplicative linear logic is NP-complete. TCS, 135:155–169, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  17. H. Mantel, C. Kreitz. A Matrix Characterization for MELL. Logics in Artificial Intelligence, JELIA’ 98, LNAI 1489, pp. 169–183, Springer, 1998.

    Google Scholar 

  18. A. Martelli and U. Montanari. An efficient unification algorithm. ACM TOPLAS, 4:258–282, 1982.

    Article  MATH  Google Scholar 

  19. M. Masseron, C. Tollu, J. Vauzeilles. Generating plans in linear logic. In Foundations of Software Technology and Theoretical Computer Science, LNCS, Springer, 1991.

    Google Scholar 

  20. D. Miller. FORUM: A Multiple-Conclusion Specification Logic. TCS, 165(1):201–232, 1996.

    Article  MATH  Google Scholar 

  21. J. Otten. ileanTAP: An Intuitionistic Theorem Prover. Proc. 6 th TABLEAUX Conference, LNAI 1227, pp. 307–312, Springer 1997.

    Google Scholar 

  22. J. Otten, C. Kreitz. T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods. Proc. 5 th TABLEAUX Workshop, LNAI 1071, pp. 244–260, 1996.

    Google Scholar 

  23. T. Tammet. Proof strategies in linear logic. JAR, 12:273–304, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  24. N. Tamura. User’s Guide of a Linear Logic Theorem Prover (llprover). Technical report. Faculty of Engineering, Kobe University, Japan, 1995.

    Google Scholar 

  25. L. Wallen. Automated deduction in nonclassical logic. MIT Press, 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. German Research Center for Artificial Intelligence (DFKI), Stuhlsatzenhausweg 3, 66123, Saarbrücken, Germany

    Heiko Mantel

  2. Fachgebiet Intellektik, Fachbereich Informatik, Darmstadt University of Technology, Alexanderstr. 10, 64283, Darmstadt, Germany

    Jens Otten

Authors
  1. Heiko Mantel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jens Otten
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Institute for Programming and Logics, University at Albany - SUNY, Albany, NY, 12222, USA

    Neil V. Murray

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mantel, H., Otten, J. (1999). linTAP : A Tableau Prover for Linear Logic. In: Murray, N.V. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1999. Lecture Notes in Computer Science(), vol 1617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48754-9_20

Download citation

  • DOI: https://doi.org/10.1007/3-540-48754-9_20

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66086-6

  • Online ISBN: 978-3-540-48754-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation