Técnicas de Prova de

UFMG - Pós-graduação em Ciência da Computação - Programação Paralela

Técnicas de Prova de $P \ensuremath{ \; leads\!{\small -}\!to\;}Q$

Basicamente temos dois tipos de regras de prova:
- regras do tipo $\ensuremath{ \; leads\!{\small -}\!to\;}$ via um comando guardado $\gamma$ , e
- Regras de fechamento (closure rules ) que nos permitem inferir asserções $\ensuremath{ \; leads\!{\small -}\!to\;}$ de outras asserções $\ensuremath{ \; leads\!{\small -}\!to\;}$ , como
  $\begin{displaymath} P \ensuremath{ \; leads\!{\small -}\!to\;}R \wedge R \ensure... ...;}Q \Longrightarrow P \ensuremath{ \; leads\!{\small -}\!to\;}Q\end{displaymath}$