Recycling Proof Patterns in Coq: Case Studies

  1. Heras, J. 1
  2. Komendantskaya, E. 1
  1. 1 University of Dundee
    info

    University of Dundee

    Dundee, Reino Unido

    ROR https://ror.org/03h2bxq36

Aldizkaria:
Mathematics in Computer Science

ISSN: 1661-8270

Argitalpen urtea: 2014

Alea: 8

Zenbakia: 1

Orrialdeak: 99-116

Mota: Artikulua

DOI: 10.1007/S11786-014-0173-1 SCOPUS: 2-s2.0-84901244669 GOOGLE SCHOLAR

Beste argitalpen batzuk: Mathematics in Computer Science

Laburpena

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. © 2014 Springer Basel.