Comparing approaches to resolution based higher-order theorem proving (Q1868166)

Four approaches to resolution-based higher-order theorem proving are investigated: Andrews' higher-order resolution approach; Huet's constrained resolution approach; higher-order E-resolution; and extensional higher-order resolution. The author focuses on Henkin completeness and full extensionality. The paper demonstrates that simply adding extensionality axioms to the search space increases the amount of blind search. Higher-order E-unification and R-resolution improves the situation but it does still not provide a general solution. Extensional higher-order resolution is the sole studied approach that can completely avoid the extensionality axioms.