Abstract
It is well-known that the set of support strategy is incomplete in paramodulation theorem provers if paramodulation into variables is forbidden. In this paper, we present a paramodulation calculus for which the combination of these two restrictions is complete, based on a lazy form of the paramodulation rule which delays parts of the unification step. The refutational completeness of this method is proved by transforming proofs given by other paramodulation strategies into set of support proofs using this new inference rule. Finally, we consider the completeness of various refinements of the method, and conclude by discussing related work and future directions.
Cite
CITATION STYLE
Snyder, W., & Lynch, C. (1991). Goal directed strategies for paramodulation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 488 LNCS, pp. 150–161). Springer Verlag. https://doi.org/10.1007/3-540-53904-2_93
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
