Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.3k answers

1.7k comments

557 users

0 votes

In the below example, why did it break d<->a first and then !b|c?

According to operator precedence, | has higher precedence then <->

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

1 Answer

+1 vote
 
Best answer
The operator precedence does not matter here. Operator precedence matters if you would consider a formula like a|b<->d which is to be read as (a|b)<->d since the disjunction has a higher precedence.  

In sequents, we have however sets of formulas on the left and right hand sides (and not just single formulas). So, you have in the example a set with two formulas !b|c and d<->a. It does not matter which one you consider for the next decomposition, any ordering will be correct. In general, it does matter however if you want to generate as few goals as possible. Note that some operators enforce a splitting into two new subgoals while others only generate a single subgoal. To reduce the effort, it would be better to prefer the latter, but for correctness, it does not matter at all.
by (170k points)
selected by

Related questions

0 votes
2 answers
asked Jan 15, 2021 in * TF "Emb. Sys. and Rob." by MS (1.1k points)
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...