3
$\begingroup$

I have been researching Ståmarck's method 1. In the paper cited here, some rules are given. Rules are made of triplets (x, y, z) such that:

y $\to$ z $\equiv$ x

where x, y and z are booleans which values are either 0 (false) or 1 (true). And rules then infer a consequence (bottom part of the rule).

For example:

$$ \frac{(x, y, 1)}{x/1} $$

means that given a triplet (x, y, 1), x has to be 1 (true). This makes sense because if the expression is $ y \to 1 $, then regardless of the value of y, the expression will be true (1). Now my question is, given the following rule:

$$ \frac{(x, x, z)}{x/1} $$

Why is it not possible to infer that z = 1 as well? If the truth table of this expression is drawn, this is the result (bear in mind that the result has to be the same value as x for it to make sense):

x | z | x -> z ($ \equiv x $)
0 | 0 | 1
0 | 1 | 1
1 | 0 | 0
1 | 1 | 1

Clearly, the only line that does not immediately lead to a contradiction is the last one, and in this case z = 1 as well.

1 Sheeran, Mary, and Gunnar Stålmarck. "A tutorial on Stålmarck’s proof procedure for propositional logic." International Conference on Formal Methods in Computer-Aided Design. Springer, Berlin, Heidelberg, 1998.

$\endgroup$
3
$\begingroup$

Yes, you are right. Having $x \leftrightarrow (x \rightarrow z)$ one can deduce that $x\equiv 1$ and $z \equiv 1$.

In the paper you cite (the link is to another one btw.), rule 6 allows only to deduce that $x\equiv 1$ holds.

But then you have the triplet $(1,1,z)$ and you can apply rule 4 $\frac{(x,1,z)}{x/z}$ to deduce $z\equiv x$, i.e., $z \equiv 1$ holds, too.

I have also seen other publications that include the conclusion $z \equiv 1$ directly in rule 6.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.