Practical Proof Search for Coq by Type Inhabitation
| Autor: | Łukasz Czajka |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Type inhabitation
business.industry Computer science 010102 general mathematics Proof search 02 engineering and technology Intuitionistic logic Type (model theory) 01 natural sciences Automation TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Dependent type theory TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Calculus 020201 artificial intelligence & image processing Direct search 0101 mathematics business |
| Zdroj: | Automated Reasoning ISBN: 9783030510534 |
| DOI: | 10.1007/978-3-030-51054-1_3 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|