Nie jesteś zalogowany |
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.
