Proof Mining with Dependent Types

TL;DR

This paper introduces a novel method that combines statistical data mining and theory exploration to analyze and automate proofs within the dependently typed language Coq, addressing a gap in existing approaches.

Contribution

It presents the first approach integrating data mining and theory exploration specifically for dependently typed proof systems like Coq.

Findings

Demonstrates effective proof analysis in Coq using the combined method.

Shows potential for automating complex proofs in dependently typed languages.

Bridges the gap between statistical and logical proof analysis techniques.

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.