Banca de QUALIFICAÇÃO: HENRIQUE TORRES DE LIMA

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE : HENRIQUE TORRES DE LIMA
DATA : 22/09/2026
HORA: 10:00
LOCAL: Remoto
TÍTULO:

Implementação de métodos de pré-processamento local e global no provador de teoremas para a lógica multimodal KSP

PALAVRAS-CHAVES:

.Lógica modal, provador de teoremas, pré-processamento

PÁGINAS: 18
RESUMO:

Esse trabalho apresenta as contribuições ao provador de teoremas multimodais KSP e descreve a linguagem e o cálculo baseado em resolução utilizados pelo provador. Foram introduzidos métodos de pré-processamento capazes de lidar com problemas de lógica global e local simultaneamente. Essa nova funcionalidade não aumenta a classe de problemas solucionáveis, mas amplia os tipos de entradas permissíveis e traz maior flexibilidade ao usuário final. Entre as alterações feitas, incluem-se ajustes no analisador sintático, nas simplificações e nas funções de transformação para a forma normal negada e forma normal separada. A validade dessas implementações será corroborada por meio de um conjunto de dados previamente rotulados contendo lógica global e local; além disso, os mesmos conjuntos de testes que aferiram o \ksp em outros artigos serão replicados. Esses testes também servirão para aferir possíveis perdas computacionais resultantes dessas novas funcionalidades.

MEMBROS DA BANCA:
Presidente - 2281452 - CLAUDIA NALON
Interna - 2358912 - CELIA GHEDINI RALHA
Externo à Instituição - ULLRICH HUSTADT - UL
Externo à Instituição - BRUNO LOPES VIEIRA - UFF