A Resolution Calculus for Second-order Logic with Eager Unification

Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012
Manchester, UK


The efficiency of the first-order resolution calculus is impaired when lifting it to higher-order logic. The main reason for that is the semi-decidability and infinitary nature of higher-order unification algorithms, which requires the integration of unification within the calculus and results in a non- efficient search for refutations. We present a modification of the constrained resolution calculus (Huet’72) which uses an eager unification algorithm while retaining completeness. The algorithm is complete with regard to bounded unification only, which for many cases, does not pose a problem in practice.