Modal Pure Type Systems

被引：5
|
作者：
Tijn Borghuis
机构：
[1] Eindhoven University of Technology,Department of Mathematics and Computing Science
来源：
Journal of Logic, Language and Information | 1998年 / 7卷 / 3期
关键词：
Knowledge representation; natural deduction; normal modal logics; typed λ-calculus;
D O I：
10.1023/A:1008254612284
中图分类号：
学科分类号：
摘要：
We present a framework for intensional reasoning in typed λ-calculus. In this family of calculi, called Modal Pure Type Systems (MPTSs), a “propositions-as-types”-interpretation can be given for normal modal logics. MPTSs are an extension of the Pure Type Systems (PTSs) of Barendregt (1992). We show that they retain the desirable meta-theoretical properties of PTSs, and briefly discuss applications in the area of knowledge representation.
引用
收藏
页码：265 / 296
页数：31
相关论文
共 50 条
  • [21] Pure type systems with subtyping (Extended abstract)
    Zwanenburg, J
    TYPED LAMBDA CALCULI AND APPLICATIONS, 1999, 1581 : 381 - 396
  • [22] Condensing lemmas for pure type systems with universes
    Jiménez, BCR
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, 1999, 1548 : 422 - 437
  • [23] Pure Type Systems without Explicit Contexts
    Geuvers, Herman
    Krebbers, Robbert
    McKinna, James
    Wiedijk, Freek
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (34): : 53 - 67
  • [24] Criteria for modal controllability of linear systems of neutral type
    Metel'skii, A. V.
    Khartovskii, V. E.
    DIFFERENTIAL EQUATIONS, 2016, 52 (11) : 1453 - 1468
  • [25] Criteria for modal controllability of linear systems of neutral type
    A. V. Metel’skii
    V. E. Khartovskii
    Differential Equations, 2016, 52 : 1453 - 1468
  • [26] Modal control in systems with distributed delay of neutral type
    Marchenko, Vladimir M.
    Yakimenko, Andrey A.
    2002, Begell House Inc. (34) : 9 - 12
  • [27] Strong normalisation in two Pure Pattern Type Systems
    Wack, Benjamin
    Houtmann, Clement
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2008, 18 (03) : 431 - 465
  • [28] The semi-full closure of Pure Type Systems
    Barthe, G
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 1998, 1998, 1450 : 316 - 325
  • [29] SYSTEMS OF TRANSFINITE TYPE THEORY BASED ON INTUITIONISTIC AND MODAL LOGICS
    BOWEN, KA
    ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1974, 20 (04): : 355 - 372
  • [30] Ml2 -: A module calculus for Pure Type Systems
    Courant, Judicael
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2007, 17 : 287 - 352
12345