You are not logged in |
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.
