This is a collection of projects completed for the Logic in Computer Science course, including:

  1. Propositional logic in Haskell (Part 1):
    • Satisfiable formulas, tautologies, disjunctive normal form (DNF), DNF-based SAT solver.
  2. Propositional logic in Haskell (Part 2):
    • Conjunctive normal form (CNF), equisatisfiable CNF (ENCF), Davis-Putnam SAT solver.
  3. SAT solving with Z3 in Python (Part 1):
    • Generating all satisfying assignments, pebbling formulas, n-queens problem.
  4. SAT solving with Z3 in Python (Part 2):
    • Shortest common superstring (SCS) problem, phase transitions for the k-SAT problem.
  5. SMT solving with Z3 in Python:
    • Łoś principle, function 91, Sudoku solver.
  6. Intuitionistic propositional logic in Agda:
    • Conjunction and disjunction proofs, de Morgan’s laws, weak Pierce’s law.
  7. Intuitionistic first order logic in Agda:
    • Universal and existential quantifier proofs, relations.

Source code