Advanced search
Start date
Betweenand


On the foundations of paraconsistent logic programming

Full text
Author(s):
Tarcísio Genaro Rodrigues
Total Authors: 1
Document type: Master's Dissertation
Press: Campinas, SP.
Institution: Universidade Estadual de Campinas (UNICAMP). Instituto de Filosofia e Ciências Humanas
Defense date:
Examining board members:
Marcelo Esteban Coniglio; Juliana Bueno Soler; Hercules de Araujo Feitosa
Advisor: Marcelo Esteban Coniglio
Abstract

Logic Programming arises from the interaction between Logic and the Foundations of Computer Science: first-order theories can be seen as computer programs. Logic Programming have been broadly used in some branches of Artificial Intelligence such as Knowledge Representation and Commonsense Reasoning. From this, a wide research activity has been developed in order to define paraconsistent Logic Programming systems, that is, systems in which it is possible to deal with contradictory information. However, no such existing approaches has a clear logical basis. The basic question is to know what are the paraconsistent logics underlying such approaches. The present dissertation aims to establish a clear and solid conceptual and logical basis for developing well-founded systems of Paraconsistent Logic Programming. In that sense, this text can be considered as the first (and successful) stage of an ambitious research programme. One of the main thesis of the present dissertation is that the Logics of Formal Inconsistency (LFI's), which encompasses a broad family of paraconsistent logics, provide such a logical basis. As a first step towards the definition of genuine paraconsistent logic programming we shown, in this dissertation, a simplified version of the Herbrand Theorem for a first-order LFI. Such theorem guarantees the existence, in principle, of automated deduction methods for the (quantified) logics in which the theorem holds, a fundamental prerequisite for the definition of logic programming over such logics. Additionally, in order to prove the Herbrand Theorem we introduce sequent calculi for two quantified LFI's, and cut-elimination is proved for one of the systems. We also present, as an indispensable requisite for the above mentioned results, a new proof of soundness and completeness for first-order LFI's in which we show the necessity of requiring the Substitution Lemma for the respective semantics (AU)

FAPESP's process: 08/07760-2 - Paraconsistent logic programming based on Logics of Formal Inconsistency
Grantee:Tarcísio Genaro Rodrigues
Support Opportunities: Scholarships in Brazil - Master