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 条
  • [1] Pure Modal Logic of Names and Tableau Systems
    Pietruszczak, Andrzej
    Jarmuzek, Tomasz
    STUDIA LOGICA, 2018, 106 (06) : 1261 - 1289
  • [2] Pure Modal Logic of Names and Tableau Systems
    Andrzej Pietruszczak
    Tomasz Jarmużek
    Studia Logica, 2018, 106 : 1261 - 1289
  • [3] Type inference for pure type systems
    Severi, P
    INFORMATION AND COMPUTATION, 1998, 143 (01) : 1 - 23
  • [4] Pure patterns type systems
    Barthe, G
    Cirstea, H
    Kirchner, C
    Liquori, L
    ACM SIGPLAN NOTICES, 2003, 38 (01) : 250 - 261
  • [5] Parameters in pure type systems
    Bloo, R
    Kamareddine, F
    Laan, T
    Nederpelt, R
    LATIN 2002: THEORETICAL INFORMATICS, 2002, 2286 : 371 - 385
  • [6] TYPING IN PURE TYPE SYSTEMS
    JUTTING, LSV
    INFORMATION AND COMPUTATION, 1993, 105 (01) : 30 - 41
  • [7] A module calculus for pure type systems
    Courant, J
    TYPED LAMBDA CALCULI AND APPLICATIONS, 1997, 1210 : 112 - 128
  • [8] The Expansion Postponement in Pure Type Systems
    宋方敏
    Journal of Computer Science and Technology, 1997, (06) : 555 - 563
  • [9] Realizability and Parametricity in Pure Type Systems
    Bernardy, Jean-Philippe
    Lasson, Marc
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, 2011, 6604 : 108 - +
  • [10] The expansion postponement in Pure Type Systems
    Fangmin Song
    Journal of Computer Science and Technology, 1997, 12 (6) : 555 - 563
12345