Extensional Higher-Order Resolution

Abstract. In this paper we present an extensional higher-order resolution calculus that is complete relative to Henkin model semantics. The treatment of the extensionality principles

• Type: Conference
• Year: 1998
• Where: CADE
• Authors: Christoph Benzmüller, Michael Kohlhase
• Keywords: CADE 1998, Logical Reasoning, Long-standing Conjecture, Model Semantics, Practical Applicability