Exercises

Propositional Logic Informally

Propositional Logic Syntax

Propositional Logic Semantics

Normal Forms for Propositional Logic

Predicate Logic Informally

First-Order Logic Syntax

First-Order Logic Semantics

Normal Forms for First-Order Logic

Semantic Argument Method

Sets and Relations

Code contracts

Fun with Spec#

Solutions

Example of the pen-and-paper proof for an invariant to be inductive. Note that the notation is slightly different from Scala's syntax.

Exercises with Solutions

• please contact Viktor Kuncak with questions and corrections, and feel free to discuss the solutions with colleagues

• Discrete Mathematics and Its Applications by Kenneth Rosen, with Chapter 2 Sample