Cargando…

A Comprehensive Framework for Saturation Theorem Proving

We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It allows us to extend redundancy criteria so that they cov...

Descripción completa

Detalles Bibliográficos
Autores principales: Waldmann, Uwe, Tourret, Sophie, Robillard, Simon, Blanchette, Jasmin
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324260/
http://dx.doi.org/10.1007/978-3-030-51074-9_18