Cargando…
Extraction of Expansion Trees
We define a new method for proof mining by CERES (cut-elimination by resolution) that is concerned with the extraction of expansion trees in first-order logic (see Miller in Stud Log 46(4):347–370, 1987) with equality. In the original CERES method expansion trees can be extracted from proofs in norm...
| Autores principales: | , |
|---|---|
| Formato: | Online Artículo Texto |
| Lenguaje: | English |
| Publicado: |
Springer Netherlands
2018
|
| Materias: | |
| Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6380194/ https://www.ncbi.nlm.nih.gov/pubmed/30862992 http://dx.doi.org/10.1007/s10817-018-9453-9 |