Phox

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.