pttp-20210505
- PTTP is a theorem-prover for the first-order predicate calculus that uses the model elimination inference procedure and iterative deepening search. Input formulas are compiled by PTTP for direct execution by Prolog, so individual inference operations are fast.