A Certified Sound Algorithm for AC-unification Esta palestra discute como modificamos o algoritmo seminal de unificação AC de Stickel para evitar a recursão mútua e formalizamos sua terminação e solidez no assistente de prova PVS.Gabriel Silva PPGINF- UnB em 29/10/2021 Abstract This talk discusses how we have modified Stickel’s seminal AC-unification algorithm to avoid mutual recursion and formalised its termination and soundness in the PVS proof assistant. Furthermore, we discuss how Fages’ termination proof of Stickel’s al- gorithm was adapted, providing a unique elaborated measure that guarantees termination of the modified AC-unification algorithm. To the best of our knowledge, ours is the first formalised AC-unification algorithm for which soundness has been proved. Thus, our for- malisation is the first step towards a formally verified sound and complete AC-unification algorithm. Local e Data Tema: A Certified Sound Algorithm for AC-unificationPalestrante: Gabriel Silva PPGINF- UnBData: 29/10/2021 Secretaria Fale ConoscoRoteiros e ProcedimentosSolicitaçõesTelefones e e-mail Seminários Álgebra Análise Geometria Mecânica Sistemas Dinâmicos Teoria da Computação Teoria da Probabilidade Teoria dos Números
