1 resultado para Factoring

em Department of Computer Science E-Repository - King's College London, Strand, London


Relevância:

10.00% 10.00%

Publicador:

Resumo:

For first-order Horn clauses without equality, resolution is complete with an arbitrary selection of a single literal in each clause [dN 96]. Here we extend this result to the case of clauses with equality for superposition-based inference systems. Our result is a generalization of the result given in [BG 01]. We answer their question about the completeness of a superposition-based system for general clauses with an arbitrary selection strategy, provided there exists a refutation without applications of the factoring inference rule.