A Term Assignment for Polarized Bi-intuitionistic Logic and its Strong Normalization

• Autorzy: Biasi C. , Aschieri F.
• Języki publikacji: EN

Abstrakty

EN

We propose a term assignment (let calculus) for Intuitionistic Logic for Pragmatics ILP_AC, a polarized sequent calculus which includes ordinary positive intuitionistic logic LJ its dual LJ and dual negations ( )^ which allow a formula to "communicate" with its dual fragment. We prove the strong normalization property for the term assignment which follows by soundly translating the let calculus into simply typed l calculus with pairings and projections. A new and simple proof of strong normalization for the latter is also provided.

Słowa kluczowe

EN

subtractive logic; bi-intuitionistic logic; intuitionistic logic for pragmatics; lambda calculus; strong normalization

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 84, nr 2
• Strony: 185--205
• Opis fizyczny: bibliogr. 22 poz.

Twórcy

autor

Biasi C.

autor

Aschieri F.

• Department of Computer Science, Queen Mary University of London, London E1 4Ns, Great Britain,

Bibliografia

• [1] Bellin, G.: Natural Deduction and term assignment for co-Heyting algebras in dual intuitionistic logic, 2001, Submitted to the Proceedings of the Natural Deduction Conference, Rio de Janeiro July 2-6 2001.
• [2] Bellin, G., Biasi, C.: Towards a logic for pragmatics: assertions and conjectures, Journal of Logic and Computation, 14(4), 2004, 473-506.
• [3] Biasi, C.: Verso una logica degli operatori prammatici: asserzioni e congetture, Master Thesis, Computer Science, Verona, March 2003.
• [4] Crolard, T.: Extension de l'isomorphisme de Curry-Howard au traitement des exceptions (application d'une étude de la dualité en logique intuitionniste), Ph.D. Thesis, Universit Paris 7, December 1996.
• [5] Crolard, T.: Subtractive logic, Theoretical Computer Science, 254(1-2), 2001, 151-185.
• [6] Crolard, T.: A Formulae-as-Types Interpretation of Subtractive Logic, Journal of Logic and Computation, 14(4), 2004, 529-570.
• [7] Curien, P.-L., Herbelin, H.: The duality of computation, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000, SIGPLAN Notices 35(9), ACM, 2000, ISBN 1-58113-202-6.
• [8] Danos, V., Joinet, J.-B., Schellinx, H.: A New Deconstructive Logic: Linear Logic., J. Symb. Log., 62(3), 1997, 755-807.
• [9] David, R.: A short proof of the strong normalization of the simply typed lambda calculus, Http://www.lama.univ-savoie.fr/ david.
• [10] Girard, J.-Y.: A New Constructive Logic: Classical Logic, Mathematical Structures in Computer Science, 1, 1991, 255-296.
• [11] Girard, J.-Y.: On the Unity of Logic, Annals of Pure and Applied Logic, 59, 1993, 201-217.
• [12] Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types, Cambridge Univ. Press, 1989.
• [13] Gor´e, R.: Dual Intuitionistic Logic Revisited, TABLEAUX '00: Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Springer-Verlag, London, UK, 2000, ISBN 3-540-67697-X.
• [14] Herbelin, H.: A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure, Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers (L. Pacholski, J. Tiuryn, Eds.), 933, Springer, 1995, ISBN 3-540-60017-5.
• [15] Krivine, J.-L.: Lambda-calculus, types and models, Ellis Horwood, 1993.
• [16] Makkai, M., Reyes, G.: Completeness results for intuitionistic and modal logics in a categorical setting, Annals of Pure ans Applied Logic, 72, 1995, 25 - 101.
• [17] de Paiva, V., Pereira, L. C.: A New Proof System for Intuitionistic Logic, The Bulletin of Symbolic Logic, vol 1(1):101, 1995.
• [18] Rauszer, C.: Semi-Boolean algebras and their applications to intuitionistic logic with dual operations, Fundamenta Matematicae, 83, 1974, 219-249.
• [19] Rauszer, C.: Applications of Kripke models to Heyting-Brouwer Logic, Studia Logica, 36, 1977, 61-71.
• [20] Reyes, G., Zolfaghari, H.: Bi-Heyting Algebras, Toposes and Modalities, Journal of Philosophical Logic, 25(1), 1996, 25-43.
• [21] Shimura, T., Kashima, R.: Cut-Elimination Theorem for the Logic of Constant Domains., Math. Log. Q., 40, 1994, 153-172.
• [22] Troelstra, A. S., Schwichtenberg, H.: Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science), Cambridge University Press, July 2000, ISBN 0521779111.