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

868 questions

986 answers

1.4k comments

438 users

0 votes

In paper 17.02.2021, the solution to the conversion of the formula to LO2 is given. However, I could not understand how the timesteps are assigned to the LO2 formula.

I came up with the below solution while solving, as my understanding was, that F(phi) assigns timestep t1 to phi. Is the answer written below an accepted one?.

Thanks for your help.

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

1 Answer

+1 vote
 
Best answer
F[a WU b] is translated to

    ∃t1. t0≤t1 ∧ (∀t0. (t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2≤t0 → ¬b[t2])) → a[t0]))

which has a free occurrence of t0 and also bound occurrences. You may rename the bound occurrences and then you get the following

    ∃t1. t0≤t1 ∧ (∀t3. (t1≤t3 ∧ (∀t2. (t1≤t2 ∧ t2≤t3 → ¬b[t2])) → a[t3]))

If now now exchange t2 and t3, you get your formula.
by (139k points)
selected by
Thanks a lot for the explanation. As you mentioned, that exchanging t2 and t3 would yield the equation I got, I wonder if the solution I got would still be accepted.

If so, could you please tell me if any of the 3 solutions would be accepted?
Renaming bound variables does not change the meaning of a formula unless names of free variables in the scope of the quantifier are chosen. Hence, all of the formulas discussed above are equivalent to each other.
Thanks a lot for the help. It makes sense.

Related questions

Imprint | Privacy Policy
...