2
$\begingroup$

Superposition with equality resolution and equality factoring is said to be a complete calculus for first-order logic. The purpose of equality factoring is basically to get rid of paraduplicate literals like $p(X)$ | $p(Y)$, which is fine.

But all the papers I have on the topic agree that factoring applies only to positive equality. In other words, it doesn't handle paraduplicate negative literals like $\lnot p(X)$ | $\lnot p(Y)$. How do you deal with those?

1 Answers 1

2

The answer (thanks to Stephan Schulz, author of the E theorem prover, personal communication) is that factoring on positive literals suffices; together with the other inference rules, this will generate clauses that will resolve with the negative literals to solve the problem, if it can be solved at all.