Proof Generation in CDSAT

Maria Paola Bonacina
(Università degli Studi di Verona, Italy)

The main ideas in the CDSAT (Conflict-Driven Satisfiability) framework for SMT are summarized, leading to approaches to proof generation in CDSAT.

In Chantal Keller and Mathias Fleury: Proceedings Seventh Workshop on Proof eXchange for Theorem Proving (PxTP 2021), Pittsburg, USA, 11th July 2021, Electronic Proceedings in Theoretical Computer Science 336, pp. 1–4.
Published: 7th July 2021.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: