Proof mining with dependent types

Ekaterina Komendantskaya; Jonathan Heras

doi:10.1007/978-3-319-62075-6_21

Proof mining with dependent types

Ekaterina Komendantskaya^*, Jonathan Heras

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

5 Citations (Scopus)

Abstract

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.

Original language	English
Title of host publication	Intelligent Computer Mathematics. CICM 2017.
Editors	H. Geuvers, M. England, O. Hasan, F. Rabe, O. Teschke
Publisher	Springer
Pages	303-318
Number of pages	16
Volume	10383
ISBN (Electronic)	978-3-319-62075-6
ISBN (Print)	9783319620749
DOIs	https://doi.org/10.1007/978-3-319-62075-6_21
Publication status	E-pub ahead of print - 28 Jun 2017
Event	10th International Conference on Intelligent Computer Mathematics - The University of Edinburgh, Edinburgh, United Kingdom Duration: 17 Jul 2017 → 21 Jul 2017 http://www.cicm-conference.org/2017/cicm.php (Conference website)

Publication series

Name	Lecture Notes in Computer Science
Volume	10383
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th International Conference on Intelligent Computer Mathematics
Abbreviated title	CICM 2017
Country/Territory	United Kingdom
City	Edinburgh
Period	17/07/17 → 21/07/17
Other	Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. Separate communities have developed to investigate and build computer based systems for computer algebra, automated deduction, and mathematical publishing as well as novel user interfaces. While all of these systems excel in their own right, their integration can lead to synergies offering significant added value. The Conference on Intelligent Computer Mathematics (CICM) offers a venue for discussing and developing solutions to the great challenges posed by the integration of these diverse areas.
Internet address	http://www.cicm-conference.org/2017/cicm.php (Conference website)

Keywords

Clustering
Coq
Dependent types
Interactive theorem proving
Machine learning
Tactics
Theory exploration

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-62075-6_21

Cite this

@inbook{aff25e73a3ab4240abf3b1f1ecc33f65,

title = "Proof mining with dependent types",

abstract = "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.",

keywords = "Clustering, Coq, Dependent types, Interactive theorem proving, Machine learning, Tactics, Theory exploration",

author = "Ekaterina Komendantskaya and Jonathan Heras",

year = "2017",

month = jun,

day = "28",

doi = "10.1007/978-3-319-62075-6_21",

language = "English",

isbn = "9783319620749",

volume = "10383",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "303--318",

editor = "H. Geuvers and M. England and O. Hasan and F. Rabe and O. Teschke",

booktitle = "Intelligent Computer Mathematics. CICM 2017.",

address = "United States",

note = "10th International Conference on Intelligent Computer Mathematics, CICM 2017 ; Conference date: 17-07-2017 Through 21-07-2017",

url = "http://www.cicm-conference.org/2017/cicm.php",

}

Komendantskaya, E & Heras, J 2017, Proof mining with dependent types. in H Geuvers, M England, O Hasan, F Rabe & O Teschke (eds), Intelligent Computer Mathematics. CICM 2017.. vol. 10383, Lecture Notes in Computer Science, vol. 10383, Springer, pp. 303-318, 10th International Conference on Intelligent Computer Mathematics, Edinburgh, United Kingdom, 17/07/17. https://doi.org/10.1007/978-3-319-62075-6_21

Proof mining with dependent types. / Komendantskaya, Ekaterina; Heras, Jonathan.
Intelligent Computer Mathematics. CICM 2017.. ed. / H. Geuvers; M. England; O. Hasan; F. Rabe; O. Teschke. Vol. 10383 Springer, 2017. p. 303-318 (Lecture Notes in Computer Science; Vol. 10383).

Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

TY - CHAP

T1 - Proof mining with dependent types

AU - Komendantskaya, Ekaterina

AU - Heras, Jonathan

PY - 2017/6/28

Y1 - 2017/6/28

N2 - 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.

AB - 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.

KW - Clustering

KW - Coq

KW - Dependent types

KW - Interactive theorem proving

KW - Machine learning

KW - Tactics

KW - Theory exploration

UR - http://www.scopus.com/inward/record.url?scp=85025155806&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-62075-6_21

DO - 10.1007/978-3-319-62075-6_21

M3 - Chapter (peer-reviewed)

AN - SCOPUS:85025155806

SN - 9783319620749

VL - 10383

T3 - Lecture Notes in Computer Science

SP - 303

EP - 318

BT - Intelligent Computer Mathematics. CICM 2017.

A2 - Geuvers, H.

A2 - England, M.

A2 - Hasan, O.

A2 - Rabe, F.

A2 - Teschke, O.

PB - Springer

T2 - 10th International Conference on Intelligent Computer Mathematics

Y2 - 17 July 2017 through 21 July 2017

ER -

Proof mining with dependent types

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this