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 ].

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 ...

Start Free Trial

No credit card required