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 条
  • [1] A simple soundness proof for dependent object types
    Rapoport M.
    Kabir I.
    He P.
    Lhoták O.
    2017, Association for Computing Machinery (01)
  • [2] PROOF MINING IN Lp SPACES
    Sipos, Andrei
    JOURNAL OF SYMBOLIC LOGIC, 2019, 84 (04) : 1612 - 1629
  • [3] Proof mining in functional analysis
    Kohlenbach, U
    NEW COMPUTATIONAL PARADIGMS, 2005, 3526 : 233 - 234
  • [4] Attributive types for proof erasure
    Xi, Hongwei
    TYPES FOR PROOFS AND PROGRAMS, 2008, 4941 : 188 - 202
  • [5] Types of Dialogue and Burdens of Proof
    Walton, Douglas
    COMPUTATIONAL MODELS OF ARGUMENT: PROCEEDINGS OF COMMA 2010, 2010, 216 : 13 - 24
  • [6] CORRECTNESS PROOF FOR THE WAM WITH TYPES
    BEIERLE, C
    BORGER, E
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 626 : 15 - 34
  • [7] Refinement Types as Proof Irrelevance
    Lovas, William
    Pfenning, Frank
    TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2009, 5608 : 157 - 171
  • [8] Proof of Contribution: A Modification of Proof of Work to Increase Mining Efficiency
    Xue, Tengfei
    Yuan, Yuyu
    Ahmed, Zahir
    Moniz, Krishna
    Cao, Ganyuan
    Wang, Cong
    2018 IEEE 42ND ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1, 2018, : 636 - 644
  • [9] Mining with Proof-of-Probability in Blockchain
    Kim, Sungmin
    Kim, Joongheon
    PROCEEDINGS OF THE 2018 ACM ASIA CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (ASIACCS'18), 2018, : 841 - 843
  • [10] PROOF OF CONCEPT SEEN FOR OCEAN MINING
    WENZEL, JG
    SEA TECHNOLOGY, 1979, 20 (01) : 26 - 27
12345