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 条
  • [11] An application of proof mining to nonlinear iterations
    Leustean, Laurentiu
    ANNALS OF PURE AND APPLIED LOGIC, 2014, 165 (09) : 1484 - 1500
  • [12] Proof of efficacy trials: seizure types
    Ben-Menachem, E
    EPILEPSY RESEARCH, 2001, 45 (1-3) : 31 - 34
  • [13] Proof reuse with extended inductive types
    Boite, O
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2004, 3223 : 50 - 65
  • [14] A SHORT PROOF OF THE LAW OF CONVERGENCE OF TYPES
    CUESTA, JA
    MATRAN, C
    SANKHYA-THE INDIAN JOURNAL OF STATISTICS SERIES A, 1990, 52 : 259 - 260
  • [15] Understanding ownership types with dependent types
    Cameron, Nicholas
    Drossopoulou, Sophia
    Noble, James
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2013, 7850 : 84 - 108
  • [16] Preventing proof-of-work mining attacks
    Azimy, Hamid
    Ghorbani, Ali A.
    Bagheri, Ebrahim
    Information Sciences, 2022, 608 : 1503 - 1523
  • [17] Light monotone Dialectica methods for proof mining
    Hernest, Mircea-Dan
    MATHEMATICAL LOGIC QUARTERLY, 2009, 55 (05) : 551 - 561
  • [18] Preventing proof-of-work mining attacks
    Azimy, Hamid
    Ghorbani, Ali A.
    Bagheri, Ebrahim
    INFORMATION SCIENCES, 2022, 608 : 1503 - 1523
  • [19] On the removal of weak compactness arguments in proof mining
    Ferreira, Fernando
    Leustean, Laurentu
    Pinto, Pedro
    ADVANCES IN MATHEMATICS, 2019, 354
  • [20] Proof Learning in PVS With Utility Pattern Mining
    Nawaz, M. Saqib
    Fournier-Viger, Philippe
    Zhang, Ji
    IEEE ACCESS, 2020, 8 (08): : 119806 - 119818
12345