Proof mining with dependent types

DOI10.1007/978-3-319-62075-6_21MaRDI QIDQ2364689zbMATH OpenOpenAlexFDO

Authors Ekaterina Komendantskaya, Jónathan Heras

Publication date 21 July 2017

Full work available at URL https://arxiv.org/abs/1705.04680

zbMATH Keywords

clusteringCoqdependent typesinteractive theorem provingmachine learningtacticstheory exploration

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05)

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.

Recommendations

• scientific article; zbMATH DE number 6528605
• Dependencies in formal mathematics: applications and extraction for Coq and Mizar
• Recycling proof patterns in Coq: case studies
• Dependently Typed Programming Based on Automated Theorem Proving
• scientific article; zbMATH DE number 6296049

Cites work

• Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence
• An introduction to small scale reflection in Coq
• ATP and presentation service for Mizar formalizations
• Computing persistent homology within Coq/SSReflect
• Conjecture synthesis for inductive theories
• Hipster: integrating theory exploration in a proof assistant
• Learning-assisted theorem proving with millions of lemmas
• Lemma Mining over HOL Light
• MaSh: machine learning for Sledgehammer
• Mining state-based models from proof corpora
• Pattern recognition and machine learning.
• Proof-pattern recognition and lemma discovery in ACL2
• Recycling proof patterns in Coq: case studies
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• SEPIA: search for proofs using inferred automata
• Towards Algorithmic Cut-Introduction

Cited in

(1)

• Dependencies in formal mathematics: applications and extraction for Coq and Mizar

Describes a project that uses

Uses Software

• Coq
• PRMLT
• WEKA
• ML4PG
• MaSh
• Coq/SSReflect
• Hipster
• SEPIA
• CoqHammer
• GitHub
• IsaCoSy

This page was built for publication: Proof mining with dependent types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2364689)