Computing logical consequence in Lukasiewicz infinitely-valued logic

• Grant number: 21/10134-0
• Support Opportunities: Scholarships abroad - Research Internship - Post-doctor
• Start date: March 01, 2022
• End date: November 30, 2022
• Field of knowledge: Physical Sciences and Mathematics - Computer Science - Computing Methodologies and Techniques
• Principal Investigator: Marcelo Finger
• Grantee: Sandro Márcio da Silva Preto
• Supervisor: Felip Manya
• Host Institution: Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brazil
• Institution abroad: Instituto de Investigación en Inteligencia Artificial (IIIA), Spain
• Associated to the scholarship: 21/03117-2 - Formal verification of neural networks via Lukasiewicz infinitely-valued logic, BP.PD

Abstract

Although there are many literature and already implemented routines for treating the problems of satisfiability and validity of formulas in the Lukasiewicz Infinitely-valued Logic, we are unaware of works dealing with the problem of deciding the validity of a logical consequence in such logical system. This research project aims first to establish and implement algorithms for this problem in three different approaches. In the first approach, the problem will be reduced to a satisfiability modulo theory problem; in the second one, it will be reduced to a classical satisfiability problem; and in the third one, it will be reduced to the problem of satisfiability of signed conjunctive normal form formulas. Experiments will be conducted in all the implementations in order to rate and compare them according to their efficiency. (AU)