Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:proofs_and_induction [2008/02/20 22:22] vkuncak |
sav08:proofs_and_induction [2008/02/21 12:31] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Informal Proofs and Mathematical Induction ====== | ====== Informal Proofs and Mathematical Induction ====== | ||
- | |||
===== Proof Rules ===== | ===== Proof Rules ===== | ||
Line 78: | Line 77: | ||
Instead of proving a goal, you can assume its negation and prove any remaining goals (this generalizes proof by contradiction). | Instead of proving a goal, you can assume its negation and prove any remaining goals (this generalizes proof by contradiction). | ||
\[ | \[ | ||
- | \frac{\lnot P \vdash\} | + | \frac{\lnot P \vdash} |
{\vdash P} | {\vdash P} | ||
\] | \] | ||
Line 130: | Line 129: | ||
===== Using Proof Rules in Isabelle ===== | ===== Using Proof Rules in Isabelle ===== | ||
+ | |||
+ | [[Isabelle theorem prover]] implements these rules. It names them: | ||
+ | * conjE, conjI, disjE, disjI1, disjI2, impE, impI, allE, allI, exE, exI | ||
+ | |||
+ | The "E" (elimination) rules are for constructs on left-hand side, and "I" (introduction) rules are for constructs on right-hand side. | ||
+ | |||
+ | More information: [[http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf|Isabelle tutorial]], Chapter 5 "The Rules of the Game". | ||
+ | |||
+ | Demo: Proving above example in Isabelle. | ||
===== Completeness for First-Order Logic ===== | ===== Completeness for First-Order Logic ===== | ||
Line 152: | Line 160: | ||
\[ | \[ | ||
- | \frac{\forall n. ((\forall k < n. P(k)) \rightarrow P(n))} | + | \frac{\forall n \in \mathbb{N}. ((\forall k < n. P(k)) \rightarrow P(n))} |
- | {\forall n. P(n)} | + | {\forall n \in \mathbb{N}. P(n)} |
\] | \] | ||
- | Deriving one induction from another. | ||
==== Structural Induction ===== | ==== Structural Induction ===== | ||
* [[Calculus of Computation Textbook]], Chapter 4 (some example refer to previous chapters, if you do not understand them, ignore them for now) | * [[Calculus of Computation Textbook]], Chapter 4 (some example refer to previous chapters, if you do not understand them, ignore them for now) | ||
- |