This paper presents two approaches to primitive equality treatment in higher-order (HO) automated theorem proving: a calculus #epsilon# P adapting traditional first-order (FO) paramodulation [RW69], and a calculus #epsilon# RU #epsilon# adatping FO RUE-Resolution [Dig79] to classical type theory, i.e., HO logic based on Church's simply typed #lambda# -calculus. #epsilon# P and #epsilon# RU #epsilon# extend the extensional HO resolution approach #epsilon# R [BK98a]. In order to reach Henkin completeness without the need for additional extensionality axioms both calculi employ new, positive extensionality rules analogously to the respective negative ones provided #epsilon# R that operate on unification constraints. As the extensionality rules have an intrinsic and unavoidable difference-reducing character the HO paramodulation approach loses its pure term-rewriting character. On the other hand examples demonstrate that the extensionality rules harmonise quite well with the difference-reducing HO RUE-resolution idea.
展开▼
