## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

No credit card required

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

## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

No credit card required