Computando consequência lógica na lógica infinitamente-valorada de Lukasiewicz

• Processo: 21/10134-0
• Modalidade de apoio: Bolsas no Exterior - Estágio de Pesquisa - Pós-Doutorado
• Data de Início da vigência: 01 de março de 2022
• Data de Término da vigência: 30 de novembro de 2022
• Área de conhecimento: Ciências Exatas e da Terra - Ciência da Computação - Metodologia e Técnicas da Computação
• Pesquisador responsável: Marcelo Finger
• Beneficiário: Sandro Márcio da Silva Preto
• Supervisor: Felip Manya
• Instituição Sede: Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brasil
• Instituição Anfitriã: Instituto de Investigación en Inteligencia Artificial (IIIA), Espanha
• Vinculado à bolsa: 21/03117-2 - Verificação formal de redes neurais via lógica infinitamente-valorada de Lukasiewicz, BP.PD
• Assunto(s): Consequência lógica Lógicas não clássicas Lógica computacional Inteligência artificial
• Palavra(s)-Chave do Pesquisador: Consequência Lógica | Dedução automática | Lógica Infinitamente-valorada de Lukasiewicz | Lógicas não clássicas | Lógica Computacional e Inteligência Artificial

Resumo

Embora haja considerável literatura e rotinas já implementadas para tratar os problemas de satisfatibilidade e validade de fórmulas na Lógica Infinitamente-valorada de Lukasiewicz, não literatura conhecida que lide com o problema de decidir a validade de uma consequência lógica neste sistema lógico. Este projeto de pesquisa tem por primeiro objetivo estabelecer e implementar algoritmos para este problema em três diferentes abordagens. Na primeira abordagem, o problema será reduzido ao problema de satisfatibilidade modulo teoria; na segunda abordagem, será reduzido a um problema de satisfatibilidade clássica; e na terceira satisfatibilidade, será reduzido ao problema de satisfatibilidade de fórmulas em forma normal conjuntiva assinalada. Serão conduzidos experimentos em todas as implementações com o objetivo de avaliar e compará-las de acordo com suas eficiências. (AU)