Intuitionistic SAT solver

Speaker(s)

Konrad Zdanowski

Affiliation

Cardinal Stefan Wyszynski University

Date

Jan. 28, 2022, 12:15 p.m.

Room

room 5820

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

I will present an article by F. Besson, Itauto: An Extensible Intuitionistic SAT Solver, which was presented at the conference Interactive Theorem Proving, ITP 2021 (url: https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13904 ). The author presents an implementation of an intuitionistic SAT solver for propositional logic with equality in Coq. I will try to outline the basic theoretical properties of the SAT solver as well as some algorithmic techniques employed in its implementation.

---