Skolem Functions and Equality in Automated Deduction

9 years 10 months ago
Skolem Functions and Equality in Automated Deduction
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.
William McCune
Added 06 Nov 2010
Updated 06 Nov 2010
Type Conference
Year 1990
Where AAAI
Authors William McCune
Comments (0)