Tutorial on interactive theorem proving using type theory

被引：0
|
作者：
Howe, DJ [1 ]
机构：
[1] Bell Labs, Murray Hill, NJ 07974 USA
来源：
COMPUTER SCIENCE LOGIC, PROCEEDINGS | 1999年 / 1683卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
引用
收藏
页码：578 / 578
页数：1
相关论文
共 50 条
  • [11] Introduction to Milestones in Interactive Theorem Proving
    Avigad, Jeremy
    Blanchette, Jasmin Christian
    Klein, Gerwin
    Paulson, Lawrence
    Popescu, Andrei
    Snelting, Gregor
    JOURNAL OF AUTOMATED REASONING, 2018, 61 (1-4) : 1 - 8
  • [12] Interactive theorem proving with temporal logic
    Felty, A
    Thery, L
    JOURNAL OF SYMBOLIC COMPUTATION, 1997, 23 (04) : 367 - 397
  • [13] System description: TPS: A theorem proving system for type theory
    Andrews, PB
    Bishop, M
    Brown, CE
    AUTOMATED DEDUCTION - CADE-17, 2000, 1831 : 164 - 169
  • [14] TPS: A theorem-proving system for classical type theory
    Andrews, PB
    Bishop, M
    Issar, S
    Nesmith, D
    Pfenning, F
    Xi, HW
    JOURNAL OF AUTOMATED REASONING, 1996, 16 (03) : 321 - 353
  • [15] A NOTE ON INTERACTIVE THEOREM-PROVING WITH THEOREM CONTINUATION FUNCTIONS
    CHOU, CT
    IFIP TRANSACTIONS A-COMPUTER SCIENCE AND TECHNOLOGY, 1993, 20 : 59 - 69
  • [16] Tutorial: Using TPS for higher-order theorem proving and ETPS for teaching logic
    Andrews, PB
    Brown, CE
    AUTOMATED DEDUCTION - CADE-17, 2000, 1831 : 511 - 512
  • [17] Integration of automated and interactive theorem proving in ILF
    Dahn, BI
    Gehne, J
    Honigmann, T
    Wolf, A
    AUTOMATED DEDUCTION - CADE-14, 1997, 1249 : 57 - 60
  • [18] Interactive Theorem Proving Preface of the Special Issue
    Klein, Gerwin
    Gamboa, Ruben
    JOURNAL OF AUTOMATED REASONING, 2016, 56 (03) : 201 - 203
  • [19] The open calculus of constructions (Part I): An equational type theory with dependent types for programming, specification, and interactive theorem proving
    Stehr, MO
    FUNDAMENTA INFORMATICAE, 2005, 68 (1-2) : 131 - 174
  • [20] The open calculus of constructions (Part II): An equational type theory with dependent types for programming, specification, and interactive theorem proving
    Stehr, MO
    FUNDAMENTA INFORMATICAE, 2005, 68 (03) : 249 - 288
12345