Minha monografia contem uma secao sobre Z/Eves no capitulo 2. Abaixo segue o link para download:https://dl.dropboxusercontent.com/u/11299884/Monografia/monografia_printed.pdf Ola, uma dica para quem tiver interesse em saber mais sobre a forma normal prenex, usada pelo Z/Eves para remover quantificadores de uma expressao:http://pt.wikipedia.org/wiki/Forma_normal_prenex Sejam P e Q schemas equivalentes. Para mostrar a equivalencia entre estes schemas usando Z/Eves deve ser provado o predicado:P \iff QUma forma tipica de mostrar esta equivalencia e dividi-la em duas partes:1. P \implies Q2. Q \implies PPara transformar o predicado P \iff Q nos predicados 1 e 2, o usuario pode entrar com os seguintes comandos de prova:slip PrewritecasesrewriteNeste ponto o predicado 1 foi obtido.nextsplit QrewriteNeste ponto o predicado 2 foi obtido.Agora, e somente provar os predicados. Para alternar entre eles utiliza-se o comando next. Ola,Estou com uma duvida sobre o mecanismo de funcionamento do Z/EVES e irei de compartilha-la com voces. O problema que irei descrever ocorre quando existem duas regras de reescrita, tal que o que a primeira regra reescreve A por B, e a segunda regra reescreve B por A. Eu esperava que o provador entrasse em loop caso eu deixasse as duas regras abilitadas e tentasse provar um outro teorema que tivesse o predicado A.Por que eu esperava isso?Porque o provador iria usar a regra 1 para reescrever A por B; depois usar a regra 2 para reescrever B por A; depois usar a regra 1 para reescrever A por B; e assim por diante (infinitamente).Consegui simular esta situacao no Z/EVES em dois arquivos de prova. No primeiro, o provador nao entra em loop; no segundo, o provador entra em loop. Minha duvida e: por que, no primeiro caso, o provador nao entra em loop?PRIMEIRO ARQUIVO: NoProofLoops.tex% A regra de reescrita rUnflex reescreve x \subseteq y por x \in \power y\begin{theorem}{rule rUnflex}\forall x, y: \power \num @ x \subseteq y \iff x \in \power y\end{theorem}% A regra de reescrita rUnflex2 reescreve x \in \power y por x \subseteq y\begin{theorem}{rule rUnflex2}\forall x, y: \power \num @ x \in \power y \iff x \subseteq y\end{theorem}% O teorema Test possui o padrao que permitira a regra de% reescrita rUnflex ser ativada.\begin{theorem}{Test}\forall x, y: \power \num | x \subseteq y @ x = y\end{theorem}SEGUNDO ARQUIVO: ProofLoops.tex\begin{theorem}{rule rUnflex}\forall x, y: \power \num @ x \subseteq y \iff x \in \power y\end{theorem}\begin{theorem}{rule rUnflex2}\forall x, y: \power \num @ x \in \power y \iff (\exists w: \power \num | w = y @ x\subseteq w)\end{theorem}\begin{theorem}{Test}\forall x, y: \power \num | x \subseteq y @ x = y\end{theorem}LOOP: Tente provar Test usando rewriteMinha suposicao e que o provador guarda tres estados: BeforeLastRewriteRule, AfterLastRewriteRule, AfterThisRewriteRule.IF (AfterThisRewriteRule = BeforeLastRewriteRule) THEN NotApplyThisRuleELSE ApllyThisRuleSe alguem aqui ja trabalhou com implementacao de um provador de teoremas, ou conhece alguem que ja, serei muito grato se procurar saber o real mecanismo usados para evitar proof loops e descrever este mecanismo para os leitores do blog. Dia 23 de novembro de 2001, chegou ao cinema o primeiro filme da saga Harry Potter, que desde entao, ficou conhecido como a saga do "menino que sobreviveu", e a cada dia que passava o