Comparing Approaches To Resolution Based Higher-Order Theorem Proving |
| |
Authors: | Benzmüller Christoph |
| |
Affiliation: | (1) Fachbereich Informatik, Universität des Saarlandes, D-66041 Saarbrücken, Germany |
| |
Abstract: | We investigate several approaches to resolution based automated theoremproving in classical higher-order logic (based on Church's simply typed-calculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews'higher-order resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higher-order E-resolution, and extensional higher-order resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratethe parallels and differences of the extensionality treatment of these approachesand demonstrate that extensional higher-order resolution is the sole approach thatcan completely avoid additional extensionality axioms. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|