## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

No credit card required

## Propositional logic

We study propositional logic in detail, defining its formal syntax in OCaml together with parsing and printing support. We discuss some of the key propositional algorithms and prove the compactness theorem, as well as indicating the surprisingly rich applications of propositional theorem proving.

2.1 The syntax of propositional logic

Propositional logic is a modern version of Boole’s algebra of propositions as presented in Section 1.4.1 It involves expressions called formulas2 that are intended to represent propositions, i.e. assertions that may be considered true or false. These formulas can be built from constants ‘true’ and ‘false’ and some basic atomic propositions (atoms) using various logical connectives (‘not’, ...

## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

No credit card required