Skip to content

Latest commit

 

History

History
11 lines (8 loc) · 680 Bytes

README.md

File metadata and controls

11 lines (8 loc) · 680 Bytes

Tarski theorem prover

Proof of concept

  • 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.