Wybe

A proof checker embedded in F#'s computation expressions

Features and progress:

• Check proofs written in a syntax inspired by Dijkstra's predicate calculus
  • A Logical Approach to Discrete Math
    • Basic proofs
  • Lambda calculus interpreter to transform expressions
  • Sets, ∀, ∃
  • Relational calculus

Examples

Technical debt

• Leave a trace when parsing calculations in CalculationCE.fs to indicate where the parsing error happened

• implement evidence of theorem proof when the reduction of transitivity implies demonstrandum