LARA

Exercises 01

For next time, please try to bring a laptop with installed:

Background

Propositional Logic Informally

Propositional Logic Syntax

  • Scala syntax trees

Propositional Logic Semantics

  • Scala functions from booleans to booleans. Formula evaluator

Normal Forms for Propositional Logic

Proof Theory for Propositional Logic

SAT Solvers

DPLL Algorithm for SAT

Advanced SAT solving Techniques

Simple SAT Solver

Simple Encodings into Propositional Logic

Fixed-width Bitvectors

A preview of Finite-Model Finders as application of propositional logic.