关于教学型构造演算的研究
计算机科学中的逻辑
2014-08-04 v1
摘要
近年来出现了教学型命题自然演绎系统。在这些系统中，必须满足教学约束：用户必须为任何引入的概念给出一个示例。首先，我们阐述此类约束的理由以及这些“教学型”演算的性质：逻辑侧面上否定的缺失，以及计算侧面上项的“有用性”特征（通过 Curry-Howard 对应）。接着，我们构造了一个简单的构造演算 (CC) 的教学型限制，称为 CCr。我们确立了该系统的逻辑局限性，并将其计算表达能力与 Godel 系统 T 进行比较。最后，以 CCr 的逻辑局限性为指导，我们提出了教学型构造演算应是什么的形式化且通用的定义。
引用
@article{arxiv.1203.3568,
title = {Investigations on a Pedagogical Calculus of Constructions},
author = {Loïc Colson and Vincent Demange},
journal= {arXiv preprint arXiv:1203.3568},
year = {2014}
}
备注
18 pages