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



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: ). 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.