Llwytho...
Hammer for Coq: Automation for Dependent Type Theory
Hammers provide most powerful general purpose automation for proof assistants based on HOL and set theory today. Despite the gaining popularity of the more advanced versions of type theory, such as those based on the Calculus of Inductive Constructions, the construction of hammers for such foundatio...
Wedi'i Gadw mewn:
| Cyhoeddwyd yn: | J Autom Reason |
|---|---|
| Prif Awduron: | , |
| Fformat: | Artigo |
| Iaith: | Inglês |
| Cyhoeddwyd: |
Springer Netherlands
2018
|
| Pynciau: | |
| Mynediad Ar-lein: | https://ncbi.nlm.nih.gov/pmc/articles/PMC6044314/ https://ncbi.nlm.nih.gov/pubmed/30069074 https://ncbi.nlm.nih.govhttp://dx.doi.org/10.1007/s10817-018-9458-4 |
| Tagiau: |
Ychwanegu Tag
Dim Tagiau, Byddwch y cyntaf i dagio'r cofnod hwn!
|