Forma normal Prenex

Olá, uma dica para quem tiver interesse em saber mais sobre a forma normal prenex, usada pelo Z/Eves para remover quantificadores de uma expressão:

http://pt.wikipedia.org/wiki/Forma_normal_prenex

Cálculo de precondição de operações compostas

Conjectura experimental:

Dada uma operação OP sobre o estado STATE, que é formada pela disjunção das operações OP1, OP2, ..., OPn, cujas precodições OP1Sig, OP2Sig, ..., OPnSig são calculadas através dos teoremas tOP1, tOP2, ..., tOPn, é possível calcular a precondição da operação OP utilizando o algoritmo:

ENTRADA DO ALGORITMO:

1. Schemas que encapsulam precondições: OP1Sig, ..., OPnSig.
2. Schema que encapsula precondição da operação OP, isto é:
OPSig \defs OP1Sig \lor OP2Sig \lor ... OPnSig
3. Teoremas de precondições tOP1, tOP2, .., tOPn


ALGORITMO:

Build-Z/Eves-Proof-Script {
let i = 1
while (i<=n) {
split OPiSig
invoke OPiSig
cases
use tOPi with disabled (OP1, OP2, ..., OPn, STATE) prove by reduce
for EACH-COMPONENT existentially quantified in current goal do:
instantiate (COMPONENT1__0'==COMPONENT1',
COMPONENT2__0'==COMPONENT2', ...,
COMPONENTn__0'==COMPONENTn')
rewrite
next
let i = i+1
}
invoke rewrite
next
}


Prova de conceito: ToyGenericProofDesing.zip



Este tópico está aberto a discussões, dado que é um resultado experimental e sem prova. Este reasoning sobre provas foi extraído do arquivo de prova da verificação do Simple Kernel. Para estudantes do MEFES que tenham acesso aos arquivos de prova do simple kernel, podem verificar a aplicação deste reasoning na prova da precondição da operação EnqueuePRIOQ.


Nota: o formato usado para calcular a precondição das operações OP1, ..., OPn utilizado neste algoritmo, baseia-se em escrever a assinatura do teorema de precondição utilizando Schemas. Este raciocínio é explicado no artigo "Mecanizando o componente de navegação do IBM CICS: um experimento do Grande Desafio".

Challenge: Proof Loops !

Olá,

Estou com uma dúvida sobre o mecanismo de funcionamento do Z/EVES e irei de compartilhá-la com vocês. 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 situação no Z/EVES em dois arquivos de prova. No primeiro, o provador não entra em loop; no segundo, o provador entra em loop. Minha dúvida é: por que, no primeiro caso, o provador não 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 padrão que permitirá 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 rewrite


Minha suposição é que o provador guarda três estados: BeforeLastRewriteRule, AfterLastRewriteRule, AfterThisRewriteRule.

IF (AfterThisRewriteRule = BeforeLastRewriteRule) THEN
NotApplyThisRule
ELSE
ApllyThisRule


Se alguém aqui já trabalhou com implementação de um provador de teoremas, ou conhece alguém que já, serei muito grato se procurar saber o real mecanismo usados para evitar proof loops e descrever este mecanismo para os leitores do blog.

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.

Mecanizando o componente de navegação do IBMs CICS

O site do MEFES (Métodos Formais em Engenharia de Software) está hospedado em https://wiki.dcc.ufba.br/MEFES/. Neste endereço está disponível para download o artigo "Mecanizando o componente de navegação do IBMs CICS: um experimento do Grande Desafio". O artigo foi publicado na IX ERBASE e foi premiado com o terceiro lugar no Workshop de Trabalhos de Iniciação Científica e de Graduação (WTICG). A ERBASE é um evento regional promovido anualmente pela Sociedade Brasileira de Computação.

Como citar:

DIAS, D. M. ; Robson Silva ; Leo Freitas ; Adolfo Duran . Mecanizando o componente de navegação do IBMs CICS: um experimento do Grande Desafio. In: IX Escola Regional de Computação Bahia - Alagoas - Sergipe, 2009, Ilheus. Anais da IX ERBASE, 2009.