Athena Self-Study Courses

There are three available courses for learning Athena. The material for these courses consists of thoughtfully curated excerpts from the Athena book.

The three courses are labelled "Minimal", "Quick" and "Complete".

While the "Complete" sequence is recommended and can be completed in a few days of study, "Minimal" is the fastest way to get started. The "Quick" study sequence is very similar to the "Minimal" sequence, but includes additional material on a core aspect of Athena's semantics (the runtime assumption base), as well as material on a very powerful proof mechanism, implication chaining.

Below is a diagram displaying the dependency tree of the course contents, as well as the lesson sequence depending on the chosen path.

Lessons

The following links correspond to the numbered entries in the tree above. Each link navigates to a downloadable PDF file.

1. Athena Overview & Athena Introduction
2. Whirlwind Tour
3. Assumption Bases
4. Directives
5. Modules
6. Athena Programming
7. Proof Basics
8. SAT Solving
9. SMT Solving and ATPs
10. Logic Programming
11. Summary and Exercises
12. Odds and Ends
13. Pattern Matching
14. Datatypes
15. Sentential Logic
16. Equality Chaining
17. Predicate Logic
18. Implication Chaining
19. Predicate Logic Exercises

Tutorials

Blogs

• Proof Engineering Blog
• First Order Logic with Athena by Joseph Vidal-Rosset

PDFs

• Athena Basics: A Short Tutorial
• Pizza, Recursion & Induction
• Automated Theorem Proving in Athena
• Athena Language Reference

Books

• Fundamental Proof Methods in Computer Science