Proving Theorems with Athena
David R. Musser, Aytekin Vargun · 2005
1 Introduction 12 Proofs about order relations 23 Proofs about natural numbers 73.1 Term rewriting methods . . . . . . . . . . . . . . . . . . . . . 83.2 Proof by induction . . . . . . . . . . . . . . . . . . . . . . . . 113.3 Steps of a proof of an Nat inductive property. . . . . . . . . . 123.4 Basis case proof . . . . . . . . . . . . . . . . . . . . . . . . . . 123.5 Induction step proof . . . . . . . . . . . . . . . . . . . . . . . 123.6 The full proof . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 Proofs about lists 154.1 Append Nil Property . . . . . . . . . . . . . . . . . . . . . . . 154.2 Steps of a proof of a List inductive property . . . . . . . . . . 174.3 Another proof about Append . . . . . . . . . . . . . . . . . . 17