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

935 questions

1.1k answers


442 users

0 votes

To Convert [(X a) SU (F b)] to L01, 

I solved on my own and I got solution which is similar to the one generated in the teaching tool.

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

However The exam solution contains a different answer and I am wondering is that a shortened version of the solution?(2017.02 Paper)

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

1 Answer

+1 vote
Best answer
It seems that both solutions are similar, the example solution evaluates the formula at time 0 while yours starts at a general time t0. Based on that the bound variables are renamed, but then the formulas are the same, right?
by (144k points)
selected by
Yes, now I get it. Thank you for clarifying.

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
asked Aug 24, 2022 in * TF "Emb. Sys. and Rob." by CS_E (2.9k points)
Imprint | Privacy Policy