Simple dataset for proof method recommendation in Isabelle/HOL

DOI10.1007/978-3-030-53518-6_21zbMATH Open1455.68250arXiv2004.10667OpenAlexW3042276534MaRDI QIDQ2219413

Author name not available (Why is that?)

Publication date: 20 January 2021

Abstract: Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning practitioners, who often do not have much expertise in formal logic, let alone Isabelle/HOL, from achieving a large scale success in this field. In this data description, we present a simple dataset that contains data on over 400k proof method applications along with over 100 extracted features for each in a format that can be processed easily without any knowledge about formal logic. Our simple data format allows machine learning practitioners to try machine learning tools to predict proof methods in Isabelle/HOL without requiring domain expertise in logic.

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

Mathematics Subject Classification ID

No records found.

This page was built for publication: Simple dataset for proof method recommendation in Isabelle/HOL

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