sexta-feira, 17 de julho de 2009

Teoremas de equivalência

Sejam P e Q schemas equivalentes. Para mostrar a equivalência entre estes schemas usando Z/Eves deve ser provado o predicado:

P \iff Q

Uma forma tipica de mostrar esta equivalência é dividi-la em duas partes:

1. P \implies Q
2. Q \implies P

Para transformar o predicado P \iff Q nos predicados 1 e 2, o usuário pode entrar com os seguintes comandos de prova:

slip P
rewrite
cases
rewrite

Neste ponto o predicado 1 foi obtido.

next
split Q
rewrite

Neste ponto o predicado 2 foi obtido.

Agora, é somente provar os predicados. Para alternar entre eles utiliza-se o comando next.

Um comentário:

Micheluefs disse...

Cara, muito bacana que você tenha um blog sobre essa assunto. Estou começando a estudar, então pode ter certeza que pelo menos você terá alguém para discutir o assunto sempre contigo...

PS: se não fosse pela foto eu nem ia te reconhecer...

Abração,
Michel (caso não lembre, seu colega de sala de aula de metodos formais)