Cargando…

Practical Proof Search for Coq by Type Inhabitation

We present a practical proof search procedure for Coq based on a direct search for type inhabitants in an appropriate normal form. The procedure is more general than any of the automation tactics natively available in Coq. It aims to handle as large a part of the Calculus of Inductive Constructions...

Descripción completa

Detalles Bibliográficos
Autor principal: Czajka, Łukasz
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324019/
http://dx.doi.org/10.1007/978-3-030-51054-1_3
_version_ 1783551866148225024
author Czajka, Łukasz
author_facet Czajka, Łukasz
author_sort Czajka, Łukasz
collection PubMed
description We present a practical proof search procedure for Coq based on a direct search for type inhabitants in an appropriate normal form. The procedure is more general than any of the automation tactics natively available in Coq. It aims to handle as large a part of the Calculus of Inductive Constructions as practically feasible. For efficiency, our procedure is not complete for the entire Calculus of Inductive Constructions, but we prove completeness for a first-order fragment. Even in pure intuitionistic first-order logic, our procedure performs competitively. We implemented the procedure in a Coq plugin and evaluated it on a collection of Coq libraries, on CompCert, and on the ILTP library of first-order intuitionistic problems. The results are promising and indicate the viablility of our approach to general automated proof search for the Calculus of Inductive Constructions.
format Online
Article
Text
id pubmed-7324019
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73240192020-06-30 Practical Proof Search for Coq by Type Inhabitation Czajka, Łukasz Automated Reasoning Article We present a practical proof search procedure for Coq based on a direct search for type inhabitants in an appropriate normal form. The procedure is more general than any of the automation tactics natively available in Coq. It aims to handle as large a part of the Calculus of Inductive Constructions as practically feasible. For efficiency, our procedure is not complete for the entire Calculus of Inductive Constructions, but we prove completeness for a first-order fragment. Even in pure intuitionistic first-order logic, our procedure performs competitively. We implemented the procedure in a Coq plugin and evaluated it on a collection of Coq libraries, on CompCert, and on the ILTP library of first-order intuitionistic problems. The results are promising and indicate the viablility of our approach to general automated proof search for the Calculus of Inductive Constructions. 2020-06-06 /pmc/articles/PMC7324019/ http://dx.doi.org/10.1007/978-3-030-51054-1_3 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Czajka, Łukasz
Practical Proof Search for Coq by Type Inhabitation
title Practical Proof Search for Coq by Type Inhabitation
title_full Practical Proof Search for Coq by Type Inhabitation
title_fullStr Practical Proof Search for Coq by Type Inhabitation
title_full_unstemmed Practical Proof Search for Coq by Type Inhabitation
title_short Practical Proof Search for Coq by Type Inhabitation
title_sort practical proof search for coq by type inhabitation
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324019/
http://dx.doi.org/10.1007/978-3-030-51054-1_3
work_keys_str_mv AT czajkałukasz practicalproofsearchforcoqbytypeinhabitation