Skolem Functions and Equality in Automated Deduction

William McCune

We present a strategy for restricting the application of the inference rule paramodulation. The strategy applies to problems in first-order logic with equality and is designed to prevent paramodulation into subterms of Skolem expressions. A weak completeness result is presented (the functional reflexive axioms are assumed). Experimental results on problems in set theory, combinatory logic, Tarski geometry, and algebra show that the strategy can be useful when searching for refutations and when applying Knuth-Bendix completion. The emphasis of the paper is on the effectiveness of the strategy rather than on its completeness.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.