Nie jesteś zalogowany | zaloguj się

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

  • Skala szarości
  • Wysoki kontrast
  • Negatyw
  • Podkreślenie linków
  • Reset

Aktualności — Wydarzenia

SLIWOWICA

 

Intuitionistic SAT solver


Prelegent: Konrad Zdanowski

2022-01-28 12:15

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.