Tarski theorem prover

• Online interactive first-order logic theorem prover with Tarski axiom set for Euclidean geometry.
• Embed several aspects of predicate functor logic directly into the GUI. Expressed axiom schema as a monad.
• Leverage Elm type system to formally verify the design’s correctness. Explore Zipper data structure capability as an alternative method to identify generated data instead of wrapping inside the Random monad.

Roadmap

• Monad to geometrically graph the current state of theorems
• High level axioms / Birkhoff's axioms / First order axiomization of the reals.