- - - - CENAPAD-MGCO

A seguir: Prova de via com Acima: Modelos Formais: Progresso Anterior: Sistemas de Transições de

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

• Basicamente temos dois tipos de regras de prova:
  • regras do tipo via um comando guardado $\gamma$, e
  • Regras de fechamento (closure rules ) que nos permitem inferir asserções de outras asserções , como

    $$P \ensuremath{ \; leads\!{\small -}\!to\;}R \wedge R \ensure... ...;}Q \Longrightarrow P \ensuremath{ \; leads\!{\small -}\!to\;}Q$$