Phox

In automated theorem proving, PhoX is a proof assistant based on higher-order logic which is eXtensible. The user gives PhoX an initial goal and guides it through subgoals and evidence to prove that goal; internally, it constructs natural deduction trees. Each previously proven formula can become a rule for later proofs.
PhoX was originally designed and implemented by Christophe Raffalli in the OCaml programming language. He has continued to lead the current development team, a joint effort of University of... meer