## Higher-Order Tableaux

• Even though higher-order calculi for automated theorem prov-ing are rather old, tableau calculi have not been investigated yet. Thispaper presents two free variable tableau calculi for higher-order logicthat use higher-order unification as the key inference procedure. Thesecalculi differ in the treatment of the substitutional properties of equival-ences. The first calculus is equivalent in deductive power to the machine-oriented higher-order refutation calculi known from the literature, whereasthe second is complete with respect to Henkin's general models.

### Additional Services

Author: Michael Kohlhase urn:nbn:de:hbz:386-kluedo-2564 Article English 1999 1999 Technische Universität Kaiserslautern Fachbereich Informatik 004 Datenverarbeitung; Informatik

$Rev: 12793$