Jest to zbiór projektów zrealizowanych w ramach przedmiotu Logika dla Informatyków, obejmujący:
- Logikę zdaniową w Haskellu (Część 1):
- Spełnialność formuł, tautologie, dysjunkcyjna postać normalna (DNF), SAT solver oparty na DNF.
- Logikę zdaniową w Haskellu (Część 2):
- Koniunkcyjna postać normalna (CNF), równoważnie spełnialna CNF (ECNF), SAT solver oparty na algorytmie Davisa-Putnama.
- Rozwiązywanie SAT za pomocą biblioteki Z3 w Pythonie (Część 1):
- Generowanie wszystkich spełniających przypisań, formuły kamyczkowe, problem hetmanów.
- Rozwiązywanie SAT za pomocą biblioteki Z3 w Pythonie (Część 2):
- Problem najkrótszego wspólnego nadciągu (SCS), przejścia fazowe dla problemu k-SAT.
- Rozwiązywanie SMT za pomocą Z3 w Pythonie:
- Twierdzenie Łosia, funkcja 91, Sudoku solver.
- Intuicycjonistyczna logika zdaniowa w Agdzie:
- Dowody dla koniunkcji i alternatywy, prawa de Morgana, słabe prawo Pierce’a.
- Intuicycjonistyczna logika pierwszego rzędu w Agdzie:
- Dowody dla kwantyfikatorów ogólnych i egzystencjalnych, relacje.