Czasopismo
2014
|
Vol. 130, nr 1
|
125--162
Tytuł artykułu
Autorzy
Wybrane pełne teksty z tego czasopisma
Warianty tytułu
Języki publikacji
Abstrakty
We aim to establish the multi-modal logic CKn as a baseline for a constructive correspondence theory of constructive modal logics. Just like many classical multi-modal logics may be studied as theories of the basic system K obtained by model-theoretic specialisation, we envisage constructive modal logics to be derived as proof-theoretic enrichments of CKn. The system CKn would then act as a core system for constructive contextual reasoning with controlled information flow. In this paper, as a first step towards this goal, we study CKn as a type theory and introduce its computational λ-calculus, λCKn. Extending previous work on CKn, we present a cut-free contextual sequent system in the spirit of Masini’s two-dimensional generalisation of natural deduction and Brünnler’s nested sequents and give a computational interpretation for CKn following the Curry- Howard Correspondence. The associated modal type theory λCKn permits an interpretation for both the modalities □ and ⋄ of CKn as type operators with simple and independent constructors and destructors, which has been missing in the literature. It is shown that the calculus satisfies subject reduction, strong normalisation and confluence. Since normal forms can be characterised by way of a Gentzen-style typing system with sub-formula property, CKn is suitable for proof search in CKn. At the same time, λCKn enjoys natural deduction style typing which is important for programming applications. In contrast to most existing modal type theories, which are obtained as theories of the constructive modal logic S4, CKn is not bound to a particular contextual interpretation. Thus, λCKn constitutes the core of a functional language which provides static type checking of information processing to support safe contextual navigation in relational structures like those treated by description logics. We review some existing work on modal type theories and discuss their relation to λCKn.
Czasopismo
Rocznik
Tom
Strony
125--162
Opis fizyczny
Bibliogr. 48 poz.
Twórcy
autor
- Faculty of Information Systems and Applied Computer Sciences The Otto-Friedrich-University of Bamberg, Germany
autor
- Faculty of Information Systems and Applied Computer Sciences The Otto-Friedrich-University of Bamberg, Germany
Bibliografia
- [1] Alechina, N., Mendler, M., de Paiva, V., Ritter, E.: Categorical and Kripke Semantics for Constructive S4 Modal Logic, in: Proc. of Computer Science Logic 2001 (CSL 2001) (L. Fribourg, Ed.), vol. LNCS 2142, Springer Verlag, 2001, 292–307.
- [2] Appel, A. W.: Compiling with Continuations, Cambridge University Press, 1992.
- [3] Baader, F., Calvanese, D., McGuinness, D. L., Nardi, D., Patel-Schneider, P. F., Eds.: The Description Logic Handbook: Theory, Implementations and Applications, 2nd edition, Cambridge University Press, 2007.
- [4] Barber, A., Plotkin, G.: Dual Intuitionisic Linear Logic, Technical Report ECS-LFCS-96-347, University of Edinburgh, 1996.
- [5] Bellin, G., de Paiva, V., Ritter, E.: Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic, Methods for Modalities II, Amsterdam, November 2001.
- [6] Benton, N., Bierman, G., de Paiva, V.: Computational Types From a Logical Perspective, Journal of Functional Programming, 8(2), 1998.
- [7] Borghuis, V. A. J.: Coming to Terms with Modal Logic, Ph.D. Thesis, Technical University of Eindhoven, 1994.
- [8] Botazzo, L., Ferrari, M., Fiorentini, C., Fiorino, G.: A constructive semantics for ALC, Int’l Workshop on Description Logics (DL 2007) (D. Calvanese, E. Franconi, V. H. D. Lembo, B. Motik, S. Tessaris, A.-Y. Turhan, Eds.), Bolzano University Press, June 2007.
- [9] Brünnler, K.: Deep sequent systems for modal logic, Archive for Mathematical Logic, 48(6), 2009, 551–577.
- [10] Calvanese, D., Giacomo, G. D., Lenzerini, M., Nardi, D., Rosati, R.: Information Integration: Conceptual Modeling and Reasoning Support, 3rd IFCIS Conference on Cooperative Information Systems, IEEE Computer Society, 1998.
- [11] van Dalen, D.: Intuitionistic Logic, in: Handbook of Philosophical Logic (D. Gabbay, F. Guenthner, Eds.), vol. III, chapter 4, Reidel, 1986, 225–339.
- [12] Fairtlough, M., Mendler, M.: Propositional Lax Logic, Information and Computation, 137(1), August 1997, 1–33.
- [13] Fischer-Servi, G.: Semantics for a class of intuitionistic modal calculi, in: Italian Studies in the Philosophy of Science (M. L. D. Chiara, Ed.), Reidel, 1980, 59–72.
- [14] Fitch, F. B.: Intuitionistic Modal Logic with Quantifiers, Portugaliae Mathematica, 1948, 113–118.
- [15] Gabbay, D. M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional modal logics, Elsevier, 2003.
- [16] Ghani, N., de Paiva, V., Ritter, E.: Explicit Substitutions for Constructive Necessity, Automata, Languages and Programming (ICALP’98) (K. Larsen, S. Skyum, G. Winskel, Eds.), LNCS 1443, Springer, 1998.
- [17] Girard, J. Y., Lafont, Y., Taylor, P.: Proofs and Types, Cambridge University Press, 1989.
- [18] Goubault-Larrecq, J.: On Computational Interpretations of the Modal Logic S4 I. Cut Elimination, Technical report, Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe, 1996.
- [19] Goubault-Larrecq, J.: On Computational Interpretations of the Modal Logic S4 II. The lambda-evQ calculus, Technical report, Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe, 1996.
- [20] Goubault-Larrecq, J., Goubault, E.: On the geometry of intuitionistic S4 proofs, Homology, Homotopy and Applications, 5(2), 2003, 137–209.
- [21] de Groote, P.: On the strong normalisation of intuitionistic natural deduction with permutation-conversions, Information and Computation, 178(2), 2002, 441–464.
- [22] Kobayashi, S.: Monad as Modality, Theoretical Computer Science, 175, 1997, 29–74.
- [23] Luettgen, G., Mendler, M.: The Intuitionism behind Statecharts step, ACM Transactions on Computational Logic, 3(1), January 2002, 1–41.
- [24] Martini, S., Masini, A.: A Computational Interpretation of Modal Proofs, Proof Theory of Modal Logics (H. Wansig, Ed.), Kluwer, 1996.
- [25] Masini, A.: 2-sequent calculus: Intuitionism and natural deduction, Journal of Logic and Computation, 3(4), 1993, 533–562.
- [26] Mendler, M.: Constrained proofs: a logic for dealing with behavioural constraints in formal hardware verification, Workshop on Designing Correct Circuits (G. Jones, M. Sheeran, Eds.), Springer, 1991.
- [27] Mendler, M., de Paiva, V.: Constructive CK for Contexts, Context Representation and Reasoning (CRR-2005) (L. Serafini, P. Bouquet, Eds.), CEUR Proceedings, Paris, July 2005.
- [28] Mendler, M., Scheele, M.: On the Computational Interpretation of _CKn for Contextual Information Processing, Bamberger Beiträge zurWirtschaftsinformatik und Angewandten Informatik 91, The Otto-Friedrich-University of Bamberg, May 2013.
- [29] Mendler, M., Scheele, S.: Towards constructive description logics for abstraction and refinement, 21st Int’l Workshop on Description Logics (DL2008), CEUR Workshop proceedings 353, May 2008.
- [30] Mendler, M., Scheele, S.: Towards a Simply Typed CALculus for Semantic Knowledge, Logics for Agents and Mobility (LAM 2010), Edinburgh, July 2010.
- [31] Mendler, M., Scheele, S.: Towards Constructive DL for Abstraction and Refinement, Journal of Automated Reasoning, 44(3), 2010, 207–243.
- [32] Mendler, M., Scheele, S.: Cut-free Gentzen Calculus for Multimodal CK, Information and Computation, 209, 2011, 1465–1490.
- [33] Moggi, E.: Notions of Computation and Monads, Information and Computation, 93, 1991, 55–92.
- [34] Möller, R.: A functional layer for description logics: knowledge representation meets object-oriented programming, 11th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications (OOPSLA’96) (L. Anderson, J. Coplien, Eds.), ACM, 1996.
- [35] Nanevski, A., Pfenning, F., Pientka, B.: Contextual Modal Type Theory, ACM Transactions on Computational Logic, 9(3), June 2008, 1–49.
- [36] Nanevski, A., Pientka, B., Pfenning, F.: A Modal Foundation for Meta-Variables, Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN 2003), Upsaala, August 2003.
- [37] de Paiva, V.: Constructive Description Logics: What, Why and How, Context Representation and Reasoning, Riva del Garda, Italy, August 2006.
- [38] de Paiva, V., Bierman, G.: Intuitionistic Necessity Revisited, Technical Report CSRP-96-10, School of Computer Science, University of Birmingham, June 1996.
- [39] Paschke, A.: Typed Hybrid Description Logic Programs with Order-sorted semantic web type systems on OWL and RDFS, Technical report, TU Munich, December 2005.
- [40] Pfenning, F., Davies, R.: A Judgemental Reconstruction of Modal Logic, Mathematical Structures in Computer Science, 11(4), August 2001, 511–540.
- [41] Pfenning, F., Wong, H.-C.: On a modal _-calculus for S4, Proc. 11th Conf. on Mathematical Foundations of Programming Semantics (S. Brookes, M. Main, Eds.), 1, 1995.
- [42] Schacht, S., Hahn, U.: A denotational semantics for joining description logics and object-oriented programming, SCAI’97: Proceedings of the sixth Scandinavian Conference on Artificial Intelligence, IOS Press, Amsterdam, 1997.
- [43] Schürmann, C., Despeyroux, J., Pfenning, F.: Primitive recursion for higher-order abstract syntax, Theoretical Computer Science, 266(1-2), 2001, 1–57.
- [44] Simmons, H.: Derivation and Computation, Cambridge University Press, 2000.
- [45] Simpson, A. K.: The Proof Theory and Semantics of Intuitionistic Modal Logic, Ph.D. Thesis, University of Edinburgh, 1994.
- [46] Strassburger, L.: Nested sequents for intuitionistic and modal logics, Intuitionistic Modal Logics and Applications (IMLA 2011), Nancy, July 2011.
- [47] Troelstra, A. S., van Dalen, D.: Constructivism in Mathematics, vol. II, North-Holland, 1988.
- [48] Wijesekera, D.: Constructive Modal Logic I, Annals of Pure and Applied Logic, 50, 1990, 271–301
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.baztech-260cfa35-9661-4593-b824-2d184151bcad