zipperposition
A fully automatic theorem prover for typed first-order and beyond.
Description
Zipperposition is intended to be a superposition prover for full first order logic, plus some extensions (datatypes, recursive functions, arithmetic for integers and rationals, higher-order, induction). The accent is on flexibility, modularity and simplicity rather than performance, to allow quick experimenting on automated theorem proving. It generates TSTP traces or graphviz files for nice graphical display.