Hints on Proving Theorems in Twelf
Andrew W. Appel
Princeton University, February 2000
To run this tutorial, unpack the tar file,
and use Emacs to visit the README file.
You may browse the tutorial on the web by clicking the links below,
but that is a poor substitute for the interactive problemsolving
you get by running it in Emacs.
Contents:
 proving.elf

1. The mechanics of running Twelf.
2. Proving a theorem.
3. Organization of the object logic.
4. Examples using and, and_i, and_l.
5. Proof style.
 proving2.elf

6. Implication elimination and introduction; metalogic vs. object logic.
7. Or, false, not.
 proving3.elf

8. Twelf metalogic quantification.
9. Types in the object logic.
10. Creating objectlogic functions and predicates.
11. Object logic quantification.
 proving4.elf

12. Equality and congruence
13. Forward proof using "cut"
14. Twelf Traps and pitfalls
15. Objectlogic definitions
 proving5.elf

16. A case study
 proving6.elf

17. Coping with nonstrictness
18. A case study in strictness and type inference (by Kedar Swadi)
 proving7.elf

19. Extensionality & Equivalence Relations