| Full text | |
| Author(s): |
Neto, Adolfo
;
Kaestner, Celso A. A.
;
Finger, Marcelo
Total Authors: 3
|
| Document type: | Journal article |
| Source: | ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE; v. 256, p. 16-pg., 2009-12-02. |
| Abstract | |
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) | |
| FAPESP's process: | 04/14107-2 - Logical consequence and combinations of logics: fundaments and efficient applications |
| Grantee: | Walter Alexandre Carnielli |
| Support Opportunities: | Research Projects - Thematic Grants |