A carregar...
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...
Na minha lista:
| Publicado no: | Automated Reasoning |
|---|---|
| Autor principal: | |
| Formato: | Artigo |
| Idioma: | Inglês |
| Publicado em: |
2020
|
| Assuntos: | |
| Acesso em linha: | https://ncbi.nlm.nih.gov/pmc/articles/PMC7324019/ https://ncbi.nlm.nih.govhttp://dx.doi.org/10.1007/978-3-030-51054-1_3 |
| Tags: |
Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
|