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 条
  • [31] A Typed C11 Semantics for Interactive Theorem Proving
    Krebbers, Robbert
    Wiedijk, Freek
    CPP'15: PROCEEDINGS OF THE 2015 ACM CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2015, : 15 - 27
  • [32] A light-weight integration of automated and interactive theorem proving
    Kanso, Karim
    Setzer, Anton
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2016, 26 (01) : 129 - 153
  • [33] AUTOMATIC THEOREM PROVING IN SET-THEORY
    PASTRE, D
    ARTIFICIAL INTELLIGENCE, 1978, 10 (01) : 1 - 27
  • [34] BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
    Lamont, Sean
    Norrish, Michael
    Dezfouli, Amir
    Walder, Christian
    Montague, Paul
    THIRTY-EIGHTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOL 38 NO 9, 2024, : 10607 - 10615
  • [35] Automated theorem proving in quasigroup and loop theory
    Phillips, J. D.
    Stanovsky, David
    AI COMMUNICATIONS, 2010, 23 (2-3) : 267 - 283
  • [36] SPECIAL ISSUE: INTERACTIVE THEOREM PROVING AND THE FORMALISATION OF MATHEMATICS Preface
    Huet, Gerard
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2011, 21 (04) : 671 - 677
  • [37] Problem solving with interactive theorem-proving - a case study
    Jaishy, Shivashish
    Ito, Nobuhiro
    Kawabe, Yoshinobu
    2016 4TH INTL CONF ON APPLIED COMPUTING AND INFORMATION TECHNOLOGY/3RD INTL CONF ON COMPUTATIONAL SCIENCE/INTELLIGENCE AND APPLIED INFORMATICS/1ST INTL CONF ON BIG DATA, CLOUD COMPUTING, DATA SCIENCE & ENGINEERING (ACIT-CSII-BCD), 2016, : 301 - 306
  • [38] Ω-ANTS -: An open approach at combining interactive and automated theorem proving
    Benzmüller, C
    Sorge, V
    SYMBOLIC COMPUTATION AND AUTOMATED REASONING, 2001, : 81 - 97
  • [39] Learning Proof Transformations and Its Applications in Interactive Theorem Proving
    Zhang, Liao
    Blaauwbroek, Lasse
    Kaliszyk, Cezary
    Urban, Josef
    FRONTIERS OF COMBINING SYSTEMS, FROCOS 2023, 2023, 14279 : 236 - 254
  • [40] 12th international conference on interactive theorem proving
    Cohen, Liron
    Kaliszyk, Cezary
    Leibniz International Proceedings in Informatics, LIPIcs, 2021, 193
12345