O'Reilly logo

Handbook of Practical Logic and Automated Reasoning by John Harrison

Stay ahead with the world's most comprehensive technology and business learning platform.

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

Start Free Trial

No credit card required

2

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.

Start Free Trial

No credit card required