Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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|improve this question

1 Answer 1

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|improve this answer

Your Answer

 
discard

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.