SemanticProver is an implementation on a truth-functional meta-theory of logic which manipulates explicitly stored truth assignments in order to solve both propositional and metalogical problems. MetaProver.jar is our latest release which contains a GUI to generate, display, and manipulate truth assignment proofs.
Questions? Contact Kevin O'Neill at oneillkeving@gmail.com