Handbook of Automated Reasoning

5 Signed resolution

Given the concept of clauses as presented in Definition 4.7, the classical resolution principle of [Robinson 1965] is straightforwardly generalized to many-valued logic. Different variants of many-valued resolution appear in the literature. Below, we describe a first-order version of “signed resolution” as defined, e.g., in [Hähnle 1994c ].

5.1 Inference rules

The conclusion of the following inference rule:

$\frac{\begin{array}{cc}\left\{S:P\right\}\cup C_1& \left\{R:Q\right\}\cup C_2\end{array}}{\left(\left\{S\cap R:P\right\}\cup C_1\cup C_2\right)\sigma }\text{binary}\text{resolution}$

is called a binary resolvent of the variable disjoint parent clauses ...