| Texto completo | |
| Autor(es): |
Neto, Adolfo
;
Kaestner, Celso A. A.
;
Finger, Marcelo
Número total de Autores: 3
|
| 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 |