This repository contains proof engineering examples utilizing the Athena proof development language.
Some of the content is modified adaptation of examples taken from the book Fundamental Proof Methods in Computer Science.
Athena was developed by Konstantine Arkoudas at MIT where he formalized a class of languages referred to as "Denotational Proof Languages"
The predicate-logic directory contains a module of useful methods for reasoning with quantifiers.
The propositional-logic directory contains:
- A module of useful methods for propositional reasoning
- An example implementation of a dpll-based SAT solver
- An example of applying the SAT solver to the graph-coloring problem
The programming_languages directory contains examples of formal syntax & semantics of programming languages, as well implementations (and accompanying proofs of correctness) of the language (e.g., compiler, interpreter, etc.). Currently, this directory only contains a toy language for arithmetic called "Calculator Language".
It is based on chapter 17 of FPMICS with some modifications.