So True!! is a simple proof-verifier for proofs that use only first order logic written by Mitchell Holt and Joel Richardson.
Download the source files from src and build them with ghc Main.hs. The binaries created can be run given a file name as an argument, e.g. ./Main theorem.jk. See theorem.jk for an example proof.
Need to implement
Caseproof data type- using definitions and theorems in proofs and statements of theorems
- using theorems as rules
- reasoning with first order logical connectives