Proof mining with dependent types
From MaRDI portal
Publication:2364689
DOI10.1007/978-3-319-62075-6_21zbMath1367.68251arXiv1705.04680OpenAlexW2612129252MaRDI QIDQ2364689
Jónathan Heras, Ekaterina Komendantskaya
Publication date: 21 July 2017
Full work available at URL: https://arxiv.org/abs/1705.04680
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Conjecture synthesis for inductive theories
- Recycling proof patterns in Coq: case studies
- Learning-assisted theorem proving with millions of lemmas
- ATP and presentation service for Mizar formalizations
- Proof-Pattern Recognition and Lemma Discovery in ACL2
- Lemma Mining over HOL Light
- Towards Algorithmic Cut-Introduction
- Computing persistent homology within Coq/SSReflect
- Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence
- SEPIA: Search for Proofs Using Inferred Automata
- MaSh: Machine Learning for Sledgehammer
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Hipster: Integrating Theory Exploration in a Proof Assistant
- Mining State-Based Models from Proof Corpora
This page was built for publication: Proof mining with dependent types
