LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
Next revision Both sides next revision
sav08:proofs_and_induction [2008/02/20 22:24]
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 156: Line 164:
 \] \]
  
-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)