Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
up vote 2 down vote accepted

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.