Handbook of Automated Reasoning

The example above suggests the following generalization of $\mathcal{P}\mathcal{V}\mathcal{D}$ :

4.10. Definition

A set of clauses S belongs to $\mathcal{P}\mathcal{V}{\mathcal{D}}_{\tau }$ if there exists a sign renaming γ such that γ(S) belongs to $\mathcal{P}\mathcal{V}\mathcal{D}$ .

The idea behind $\mathcal{P}\mathcal{V}\mathcal{D}$ is that the positive parts are always “smaller” than the negative ones. As hyperresolution produces positive ...