Suppose there is a function in e.g. CNF form. For example:
$$ (A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E) $$
For given A,B,C,D,E values it is possible to compute the value of the function with rewriting system (like Markov algorithm), correct? The rules would be:
$\neg 1 \rightarrow 0 $
$\neg 0 \rightarrow 1$
$1 \wedge 1 \rightarrow 1$
$1 \wedge 0 \rightarrow 0$
$\ldots$
$0 \vee 0 \rightarrow 0$
$\ldots$
$(0) \rightarrow 0$
$(1) \rightarrow 1$
At the end, there should be only single char: 0 or 1. Is this correct? I was trying to find confirmation in google but without success.
The above rules could also include the initial variable—to—input-value substitution rules, like e.g. $A \rightarrow 1$.