Can we use resolution to generate equivalent formulas? (Or is the resolution theorem strictly used to check for satisfiability?)
E.g.: I have following formula: $$ \lnot((p \lor q) \land (\lnot p \lor r)\land (\lnot q \lor r)) \lor r $$
(Just for the example) - would it be correct to use resolution on $[(p \lor q)\land (\lnot p \lor r)\land (\lnot q \lor r)]$, and get $r$ ? (Which would make the whole thing $\lnot r \lor r$)
Thanks in advance!
To some extent you can, yes, but you have to be very careful.
In fact, please note that $(p \lor q)\land (\lnot p \lor r)\land (\lnot q \lor r)$ is not equivalent to $r$. It implies $r$, but it is not equivalent to $r$.
In general, whenever you derive a clause from other clauses, the derived clause is implied by the clauses, but it is not equivalent to them.
However, what is true is that the conjunction of the original clauses is equivalent to the conjunction of those clauses together with the newly derived clause. That is, as a general equivalence principle we have:
$$(P \lor Q) \land (\neg Q \lor R) \land (P \lor R) = (P \lor Q) \land (\neg Q \lor R)$$
This equivalence is better known as the Consensus Theorem, but in it you recognize a kind of Resolution, since with Resolution you can derive $P \lor R$ from $(P \lor Q) \land (\neg Q \lor R)$. But again, that does not mean that $P \lor R$ is equivalent to $(P \lor Q) \land (\neg Q \lor R)$.
Now, of course, going from $(P \lor Q) \land (\neg Q \lor R)$ to $(P \lor Q) \land (\neg Q \lor R) \land (P \lor R)$ does not at all simplify the statement .. but if simplification is your goal, you would of course go just the other way around. That is, you can simplify $(P \lor Q) \land (\neg Q \lor R) \land (P \lor R)$ to $(P \lor Q) \land (\neg Q \lor R)$, and treat that as a kind of 'reverse Resolution'.
Also, Resolution often uses some of its own simplifications that can be used to find simplified yet still equivalent formulas. For example, in resolution you can throw out any subsumed clauses. For example, the clause $\{ P, Q \} $subsumes the clause $\{P, Q, R \}$, and hence you can throw out $\{P, Q, R \}$. This actually translates into a well-known equivalence principle called Absorption:
$$P \land (P \lor Q) = P$$
So, if you regard that as a kind of 'resolution', then you can do that kind of simplification as well.
This last observation also relates to a special case of resolution, where you have a unit clause (a clause with one literal). For example, from the clauses $\{ P \}$ and $\{ \neg P, Q\}$ you can derive the new clause $Q$. Now again, this does not mean that $P \land (\neg P \lor Q)$ is equivalent to $Q$, but it does mean that $P \land (\neg P \lor Q)$ is equivalent to $P \land (\neg P \lor Q) \land Q$. But since $Q$ subsumes/absorbs $\neg P \lor Q$, it is equivalent to $P \land Q$. And that is an equivalence principle as well, called Reduction:
$$P \land (\neg P \lor Q) = P \land Q$$
So, if we regard all the equivalences as a kind of 'resolution' (they are certainly intimately related to the process of resolution), then yes, we can simplify statement into equivalent, but simpler, statements.
However, I said 'to some extent' in the beginning of the post, because you can't use resolution to show any kind of equivalence. Double Negation, or DeMorgan, for example, have little if anything to do with the basic idea of resolution.