On the expressive power of schemes

被引：0
|
作者：
Dowek, Gilles [1 ]
Jiang, Ying [2 ]
机构：
[1] INRIA, F-75214 Paris 13, France
[2] Chinese Acad Sci, State Key Lab Comp Sci, Inst Software, Beijing 100190, Peoples R China
来源：
INFORMATION AND COMPUTATION | 2011年 / 209卷 / 09期
关键词：
Natural deduction; Proof normalization; Bound variable; MODULO; PROOFS;
D O I：
10.1016/j.ic.2011.06.003
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs in various theories. Unlike lambda-calculus, the syntax of this calculus sticks closely to the syntax of proofs, in particular, no names are introduced for the hypotheses. We show that despite its non-determinism, some typed scheme-calculi have the same expressivity as the corresponding typed lambda-calculi. (C) 2011 Elsevier Inc. All rights reserved.
引用
收藏
页码：1231 / 1245
页数：15
相关论文
共 50 条
  • [1] DIFFERENCE IN EXPRESSIVE POWER BETWEEN FLOWCHARTS AND RECURSION SCHEMES
    LYNCH, NA
    BLUM, EK
    MATHEMATICAL SYSTEMS THEORY, 1979, 12 (03): : 205 - 211
  • [2] On the Expressive Power of Kernel Methods and the Efficiency of Kernel Learning by Association Schemes
    Kothari, Pravesh K.
    Livni, Roi
    ALGORITHMIC LEARNING THEORY, VOL 117, 2020, 117 : 422 - 450
  • [3] Compilation schemes: A theoretical tool for assessing the expressive power of planning formalisms
    Nebel, B
    KI-99: ADVANCES IN ARTIFICIAL INTELLIGENCE, 1999, 1701 : 183 - 194
  • [4] ON A PROVERB AND 3 FUNCTIONS OF THE EXPRESSIVE SCHEMES OF PROVERBS
    LYAPUNOV, V
    SENDEROVICH, S
    RUSSIAN LITERATURE, 1986, 19 (04) : 393 - 404
  • [5] The expressive power of adjudication
    McAdams, RH
    UNIVERSITY OF ILLINOIS LAW REVIEW, 2005, (05): : 1043 - 1121
  • [6] THE EXPRESSIVE POWER OF TRUTH
    Fischer, Martin
    Horsten, Leon
    REVIEW OF SYMBOLIC LOGIC, 2015, 8 (02): : 345 - 369
  • [7] THE POWER OF EXPRESSIVE TOUCH
    SIMINGTON, JA
    HUMANE MEDICINE, 1995, 11 (04) : 162 - 165
  • [8] The expressive power of circumscription
    Costello, T
    ARTIFICIAL INTELLIGENCE, 1998, 104 (1-2) : 313 - 329
  • [9] On the expressive power of OCL
    Mandel, L
    Cengarle, MV
    FM'99-FORMAL METHODS, 1999, 1708 : 854 - 874
  • [10] Expressive power of circumscription
    Stanford Univ, Stanford, United States
    Artif Intell, 1-2 (313-329):
12345