Cargando…
A Comprehensive Framework for Saturation Theorem Proving
A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of dynamic and static refutational completeness holds only...
| Autores principales: | , , , |
|---|---|
| Formato: | Online Artículo Texto |
| Lenguaje: | English |
| Publicado: |
Springer Netherlands
2022
|
| Materias: | |
| Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC9637109/ https://www.ncbi.nlm.nih.gov/pubmed/36353684 http://dx.doi.org/10.1007/s10817-022-09621-7 |