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

1.1k questions

1.2k answers


538 users

0 votes

Could you please explain the process in getting the final answer?. Why was the negation moved to get an Existential successor?.

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

1 Answer

+1 vote
The trick with the negation has been done to generate a conjunction of formulas in the body of the quantifier. Then, one can use the trick mentioned on the note on slide 69 of the chapter on transition systems which is as follows: If you have any formula phi and compute the negation of phi with a variable x, then phi&x is equivalent to phi[x<-1] & x where phi[x<-1] is the formula phi where all occurrences of x were replaced with 1. Analogously, phi&!x is equivalent to phi[x<-0] & !x. This trick often simplifies these calculations significantly and is therefore recommended. It is also explained in the video and the examples in the video and the slides.
by (166k points)

Related questions

Imprint | Privacy Policy