The Heuristic Theorem Prover takes as input a theorem in the
SMTLIB
format and produces the result "sat", "unsat" or "unknown". The links
on the left give more information on the system.
Send mail to
webmaster@fordocsys.com with
questions or comments about this web site.
Last modified: 02/21/06