Autor(es)

Neto, Adolfo ; Kaestner, Celso A. A. ; Finger, Marcelo

• Tipo de documento: Artigo Científico
• Fonte: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE; v. 256, p. 16-pg., 2009-12-02.

Resumo

The KE inference system is a tableau method developed by Marco Mondadori which was presented as an improvement, in the computational efficiency sense, over Analytic Tableaux. In the literature, there is no description of a theorem prover based on the KE method for the C-1 paraconsistent logic. Paraconsistent logics have several applications, such as in robot control and medicine. These applications could benefit from the existence of such a prover. We present a sound and complete KE system for C-1, an informal specification of a strategy for the C-1 prover as well as problem families that can be used to evaluate provers for C-1. The C-1 KE system and the strategy described in this paper will be used to implement a KE based prover for C-1, which will be useful for those who study and apply paraconsistent logics. (AU)

• Processo FAPESP: 04/14107-2 - Logical consequence and combinations of logics: fundaments and efficient applications
• Beneficiário: Walter Alexandre Carnielli
• Modalidade de apoio: Auxílio à Pesquisa - Temático