Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Hints on Proving Theorems in Twelf

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 problem-solving 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 object-logic functions and predicates.
11. Object logic quantification.
proving4.elf: 12. Equality and congruence
13. Forward proof using "cut"
14. Twelf Traps and pitfalls
15. Object-logic 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