A Focused Sequent Calculus for Higher-Order Logic

ABSTRACT. We present a focused intuitionistic sequent calculus for higher- order logic. It has primitive support for equality and mixes λ-term con- version with equality reasoning. Classical reasoning is enabled by ex- tending the system with rules for reductio ad absurdum and the axiom of choice. The resulting system is proved sound with respect to Church’s simple type theory. A theorem prover based on bottom up search in the calculus has been implemented. It has been tested on the TPTP higher-order problem set with good results. The problems for which the theorem prover performs best require higher-order unification more fre- quently than the average higher-order TPTP problem. Being strong at higher-order unification the system may serve as a complement to other theorem provers in the field. The theorem prover produces proofs that can be mechanically verified against the soundness proof.