Intuitionistic SAT solver

Prelegent(ci)

Konrad Zdanowski

Afiliacja

Cardinal Stefan Wyszynski University

Termin

28 stycznia 2022 12:15

Pokój

p. 5820

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

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.

---