The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover

摘要

HTP is an SMT Modulo theorem prover similar to many others. As input, HTP accepts problems using the SMT-LIB format. As output, HTP will answer either SAT, UNSAT or UNKNOWN. Alternatively, HTP can be run in a preprocessing mode in which the output is the simplified problem in SMT-LIB format. An evidence file showing the derivation in a human readable form can be produced. There is a Treeview application which shows this derivation in a tree widget making it convenient to navigate a complex proof.