Cargando…
On Definitions of Constants and Types in HOL
This paper reports on a simpler and more powerful replacement for the principles for defining new constants that were previously provided in the various HOL implementations. We discuss the problems that the new principle is intended to solve and sketch the proofs that it is conservative and that it...
| Autor principal: | |
|---|---|
| Formato: | Online Artículo Texto |
| Lenguaje: | English |
| Publicado: |
Springer Netherlands
2016
|
| Materias: | |
| Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6109768/ https://www.ncbi.nlm.nih.gov/pubmed/30174359 http://dx.doi.org/10.1007/s10817-016-9366-4 |