Analytic tableaux for higher-order logic with choice (Q438561)

The author presents a cut-free ground tableau calculus for Church's simple type theory with choice. The inference rules only operate on the top level structure of formulas. Additionally, they restrict the instantiation terms for quantifiers to a universe that depends on the current branch. Only accessible terms on the branch need to be considered in order to apply a rule. Furthermore, instantiation terms are restricted according to the type and the formulas on the branch. This means only finitely many instantiation terms need to be considered at each stage of the search. These restrictions permit to minimize the number of rules a corresponding search procedure is obligated to consider. The authors give an extension of the calculus to include if-then-else operators. Completeness of the tableau calculus relative to Henkin models is proved. The ground calculus presented in this paper was implemented in the higher-order automated theorem-prover \texttt{Satallax}.