Hoare Kalkül - Ableitungsregeln

[flosko]

hallo leute!
hab hier eine kleine frage zur ableitungsregel 1 (H1) des Hoare-Kalküls. Da steht als Bemerkung in den Folien dabei "Variablen in v<-t unquantifiziert in P und Q!".
Ist das eine Voraussetzung, dass ich diese Regel anwenden darf? was heißt das eigenltich genau? und was mach ich, wenn sie quantifiziert sind?

[locutus]

hab hier eine kleine frage zur ableitungsregel 1 (H1) des Hoare-Kalküls. Da steht als Bemerkung in den Folien dabei "Variablen in v<-t unquantifiziert in P und Q!".
Ist das eine Voraussetzung, dass ich diese Regel anwenden darf? was heißt das eigenltich genau? und was mach ich, wenn sie quantifiziert sind?
die voraussetzung für die anwendung dieser ableitungsregel ist, dass die variablen v und t in den formeln P und Q nicht durch All- oder Existenz-quantoren quantifiziert werden.

falls das beispiel mit dem hoare kalkül gelöst werden soll, dann kommt diese konstellation hoffentlich nicht vor

quantorenelimination kommt erst in theoretische informatik 2

[Neutrino]

bisher waren nie quantoren in den formeln, daher konnten die variablen nie quantifiziert vorkommen.
falls doch einmal, ist das auch kein problem: die variablen innerhalb des quantifizierten bereichs kann man (genauso wie lokale variablen in einem unterprogramm) beliebig umbenennen. daher kann man immer dafuer sorgen, dass die variablen in v<-t nicht quantifiziert vorkommen, indem man die variable unter dem quantor umbenennt.

schaetze mal das ist eher akademisch. da ich bisher nirgends ein bsp gesehen hab wo das eine rolle spielt wird's wohl fuer die pruefung nicht so brennend wichtig sein.

nu