Proof Mining with Dependent Types

被引：5
|
作者：
Komendantskaya, Ekaterina [1 ]
Heras, Jonathan [2 ]
机构：
[1] Heriot Watt Univ, Math & Comp Sci, Edinburgh, Midlothian, Scotland
[2] Univ La Rioja, Math & Comp Sci, Rioja, Spain
来源：
INTELLIGENT COMPUTER MATHEMATICS | 2017年 / 10383卷
基金：
英国工程与自然科学研究理事会;
关键词：
Interactive theorem proving; Coq; Dependent types; Tactics; Machine learning; Clustering; Theory exploration;
D O I：
10.1007/978-3-319-62075-6_21
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Several approaches exist to data-mining big corpora of formal proofs. Some of these approaches are based on statistical machine learning, and some - on theory exploration. However, most are developed for either untyped or simply-typed theorem provers. In this paper, we present a method that combines statistical data mining and theory exploration in order to analyse and automate proofs in dependently typed language of Coq.
引用
收藏
页码：303 / 318
页数：16
相关论文
共 50 条
  • [21] Proof mining in L1-approximation
    Kohlenbach, U
    Oliva, P
    ANNALS OF PURE AND APPLIED LOGIC, 2003, 121 (01) : 1 - 38
  • [22] Energy Equilibria in Proof-of-Work Mining
    Fiat, Amos
    Karlin, Anna
    Koutsoupias, Elias
    Papadimitriou, Christos
    ACM EC '19: PROCEEDINGS OF THE 2019 ACM CONFERENCE ON ECONOMICS AND COMPUTATION, 2019, : 489 - 502
  • [23] Comparison of explosion proof certificates of mining equipment
    Ünal, Mehmet Suphi
    Killioǧlu, Süleyman Yasin
    Ünver, Bahtiyar
    Madencilik, 2016, 55 (04): : 37 - 45
  • [24] An elementary proof of strong normalization for intersection types
    Silvio Valentini
    Archive for Mathematical Logic, 2001, 40 : 475 - 488
  • [25] PROOF OF DIFFERENT TYPES OF COLLAGEN IN BOVINE EYE
    SCHMUT, O
    REICH, ME
    ZIRM, M
    ALBRECHT VON GRAEFES ARCHIV FUR KLINISCHE UND EXPERIMENTELLE OPHTHALMOLOGIE, 1975, 196 (01): : 71 - 77
  • [26] An elementary proof of strong normalization for intersection types
    Valentini, S
    ARCHIVE FOR MATHEMATICAL LOGIC, 2001, 40 (07) : 475 - 488
  • [27] A new proof of the multidimensional convergence of types theorem
    Neuenschwander, D
    STATISTICS & PROBABILITY LETTERS, 1997, 33 (01) : 85 - 88
  • [28] Proof of efficacy trials: seizure types - Discussion
    Schmidt, D
    EPILEPSY RESEARCH, 2001, 45 (1-3) : 35 - 36
  • [29] A coinductive completeness proof for the equivalence of recursive types
    Cardone, F
    THEORETICAL COMPUTER SCIENCE, 2002, 275 (1-2) : 575 - 587
  • [30] Mining Dependent Items
    Lei, Hansheng
    Hu, Yamin
    Luo, Wenjian
    Pan, Cheng Chang
    2018 1ST INTERNATIONAL CONFERENCE ON DATA INTELLIGENCE AND SECURITY (ICDIS 2018), 2018, : 103 - 109
12345