A crucial way for reducing the search space in automated deduction are the so-called selection strategies: in each clause, the subset of selected literals are the only ones involved in inferences. For first-order Horn clauses without equality, resolution is complete with an arbitrary selection of one single literal in each clause [dN96]. For Horn clauses with built-in equality, i.e., paramodulation-based inference systems, the situation is far more complex. Here we show that if a paramodulation-based inference system is complete with eager selection of negative equations and, moreover, it is compatible with equality constraint inheritance, then it is complete with arbitrary selection strategies. A first important application of this result is the one for paramodulation wrt. non-monotonic orderings, which was left open in [BGNR99]. © 2011 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Bofill, M., & Godoy, G. (2001). On the completeness of arbitrary selection strategies for paramodulation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2076 LNCS, pp. 951–962). Springer Verlag. https://doi.org/10.1007/3-540-48224-5_77
Mendeley helps you to discover research relevant for your work.