0 votes

In the following diagram, the split is based on <-> operator but considering the precedence of the operators, shouldn't we split based on '|/or'?

By doing with '|' it changes the answers for satisfiability/validity

in * TF "Emb. Sys. and Rob." by (250 points)

2 Answers

+2 votes
Best answer
There is a comma in between the two (sub-)formulas. A comma on the left is like an and. That means that the or and the equality wouldn't be interlocked. Thus, the precedence isn't applied here. You can process any of the available formulas in any order.

Also, I don't see the difference in the result.If I first process the or, I get a split. One side with a b on the right and the other one with a d on the left. They both have the same equality on the left. If I process that, I get a split like the one in the example you showed and the result is the same. (the order or the nodes might be different though)
by (24.7k points)
selected by
+1 vote

Martin is perfectly right. To see that, look at the two proof trees below:

by (92.2k points)
Imprint | Privacy Policy