2013/01/25 by Jónathan Heras, Ekaterina Komendantskaya, Heras, Jónathan +1
Computer Science · Decision Sciences · #Advanced Database Systems and Queries #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Machine Learning (cs.LG) #Scientific Computing and Data Management #Semantic Web and Ontologies #cs.AI #cs.LG #cs.LO
paper · pdf · doi:10.48550/arxiv.1301.6039
openalex publication_date 2013/01/25 · arxiv created 2014/03/07 · arxiv updated 2014/03/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Development of Interactive Theorem Provers has led to the creation of big libraries and varied infrastructures for formal proofs. However, despite (or perhaps due to) their sophistication, the re-use of libraries by non-experts or across domains is a challenge. In this paper, we provide detailed case studies and evaluate the machine-learning tool ML4PG built to interactively data-mine the electronic libraries of proofs, and to provide user guidance on the basis of proof patterns found in the existing libraries.