Skip to main content

Logic of predicates with explicit substitutions

  • Contributed Papers
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1996 (MFCS 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1113))

Abstract

We present a non-commutative linear logic — the logic of predicates with equality and explicit substitutions. Thus, the position of linear logic with respect to the usual logic is given a new explanation.

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

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Cardelli, L., Curien, P.-L. and J-J. Lévy. Explicit substitutions. ACM Conf. on Principles of Programming Languages, San Francisco, 1990.

    Google Scholar 

  2. Avron, A. Simple consequence relations. Information & Computation, Vol 92, No 1, pp. 105–139, May 1991.

    Google Scholar 

  3. Basin, D., Matthews, S., L.Vigano. A modular presentation of modal logics in a logical framework. Proc. 1st Isabelle User Workshop, pp. 137–148, Cambridge, 1995.

    Google Scholar 

  4. Bednarczyk, M. A. Quasi quantales. GDM Research Report, ICS PAS, 1994.

    Google Scholar 

  5. Bednarczyk, M. A. and T. Borzyszkowski Towards program development with Isabelle. Proc. 1st Isabelle User Workshop, pp.101–121, Cambridge, 1995.

    Google Scholar 

  6. Bednarczyk, M. A. Logic of predicates versus linear logic. ICS PAS Reports, N∘ 795, December 1995.

    Google Scholar 

  7. Brown, C. and D. Gurr. Relations and non-commutative linear logic. To appear in J. of Pure and Applied Algebra

    Google Scholar 

  8. Gallier, J. Logic for Computer Science. Foundations of Automatic Theorem Proving. Harper & Row, New York, 1986.

    Google Scholar 

  9. Gallier, J. Constructive logics. Part II: linear logic and proof nets. Research Report, CIS, University of Pennsylvania, 1992.

    Google Scholar 

  10. Girard, J.-Y. Linear logic. Theoretical Computer Science, 50 (1987), pp 1–102.

    Article  Google Scholar 

  11. Girard, J.-Y. and Y. Lafont. Linear logic and lazy computation. In: Proc. TAP-SOFT'87 (Pisa), vol. 2, LNCS 250, Springer Verlag, 1987, pp 52–66.

    Google Scholar 

  12. Girard, J.-Y., Lafont, Y. and P. Taylor. Proofs and Types. volume 7 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989.

    Google Scholar 

  13. Girard, J.-Y. Linear logic: its syntax and semantics. In Advances of Linear Logic, 1995.

    Google Scholar 

  14. Lescane, P. From λσ to λν a journey through calculi of explicit substitutions. ACM Conf. on Principles of Programming Languages, San Portland, 1994.

    Google Scholar 

  15. Mendelson, E. Introduction to Mathematical Logic. D. Van Nostrand Company, 1964.

    Google Scholar 

  16. Poigné, A. Basic Category Theory. In Handbook of Logic in Computer Science. Vol I. Clarendon Press, Oxford, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Wojciech Penczek Andrzej Szałas

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bednarczyk, M.A. (1996). Logic of predicates with explicit substitutions. In: Penczek, W., Szałas, A. (eds) Mathematical Foundations of Computer Science 1996. MFCS 1996. Lecture Notes in Computer Science, vol 1113. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61550-4_148

Download citation

  • DOI: https://doi.org/10.1007/3-540-61550-4_148

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics