Higher-order tableaux

Even though higher-order calculi for automated theorem proving are rather old, tableau calculi have not been investigated yet. This paper presents two free variable tableau calculi for higher-order logic that use higher-order unification as the key inference procedure. These calculi differ in the treatment of the substitutional properties of equivalences. The first calculus is equivalent in deductive power to the machine-oriented higher-order refutation calculi known from the literature, whereas the second is complete with respect to Henkin's general models.