Download Read the Stdm User Manual

Contents
0 Getting Started
Web Addresses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Instructor’s Guide . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Running Haskell 98 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5
5
5
6
1 Introduction to Haskell
7
2 Propositional Logic
Logical Operators . . . . . . . . . . .
Using the Proof Checker . . . . . . .
Propositions . . . . . . . . . . .
Theorems . . . . . . . . . . . .
Inferences . . . . . . . . . . . .
Assumptions . . . . . . . . . . .
Inferences on the And operator
Inferences on the Or operator .
Inferences on Implication . . . .
Inferences on Identity and False
Represention of Proofs . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
9
9
10
10
11
12
12
12
13
14
14
15
3 Predicate Logic
17
4 Set Theory
19
5 Recursion
Recursion Over Lists . . . . . . .
Higher Order Recursive Functions
Recursion Over Trees . . . . . . .
Peano Arithmetic . . . . . . . . .
Data Recursion . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
23
23
24
24
26
28
6 Inductively Defined Sets
31
7 Induction
33
8 Relations
35
9 Functions
37
3