Lógica dinâmica proposicional com armazenamento, recuperação e composição paralela: uma formalização em assistente de provas.

Abstract

Esta dissertação desenvolve fundamentos teóricos e computacionais para a Lógica Dinâmica Proposicional com Armazenamento e Recuperação (RSPDL₀), uma extensão da PDL clássica que incorpora operadores para manipulação de estado. A motivação surge da necessidade de formalismos adequados para verificação de sistemas que implementam operações de salvamento e restauração de estado, fundamentais em linguagens imperativas modernas. A RSPDL₀ introduz quatro operadores primitivos: s₁ e s₂ para armazenamento, r₁ e r₂ para recuperação. Estes operadores modelam estados como pares ordenados, permitindo armazenar componentes e recuperá-las posteriormente. A semântica utiliza conjuntos estruturados (S, E, ⋆), uma generalização da semântica de Kripke com um conjunto S de estados, relação de equivalência E, e operação injetiva ⋆ para construir estados compostos. O fragmento estudado corresponde à RSPDL₀, que omite os operadores de iteração, teste e composição paralela da PRSPDL completa, focando nos operadores fundamentais de manipulação de estado. Desenvolvemos um sistema axiomático completo que captura as propriedades essenciais destes operadores através de esquemas finitos. Demonstramos corretude através de lemas que estabelecem validade semântica dos axiomas em frames próprios. A completude segue a construção canônica de Henkin-Lindenbaum, relacionando satisfação semântica com derivabilidade sintática via Lema da Verdade. A formalização em Lean 4 demonstra como lógicas modais complexas podem ser implementadas em sistemas de tipos dependentes. Utilizamos tipos indutivos mutuamente recursivos para sintaxe, classes de tipos para estruturas algébricas, e táticas para construção de provas. Esta correspondência entre teoria matemática e implementação verificada valida os resultados obtidos. A implementação atual estabelece fundações sintáticas e semânticas, propriedades do sistema dedutivo, e formaliza parcialmente corretude e completude. O Lema da Verdade para casos modais complexos e a verificação de propriedades do modelo canônico permanecem como trabalho futuro, juntamente com extensões para o fragmento completo da PRSPDL e aplicações em verificação de software.