| Full text | |
| Author(s): |
Carnielli, Walter
;
Matulovic, Mariana
Total Authors: 2
|
| Document type: | Journal article |
| Source: | ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE; v. 305, p. 16-pg., 2014-07-11. |
| Abstract | |
The method for automatic theorem proving proposed in [6], called Polynomial Ring Calculus, is an algebraic proof mechanism based on handling polynomials over finite fields. Although useful in general domains, as in first-order logic, certain non-truth-functional logics and even in modal logics (see [1]), the method is particularly apt for deterministic and non-deterministic many-valued logics, as shown here. The aim of the present paper is to show how the method can be extended to any finite-valued non-deterministic semantics, and also to explore the computational character of the method through the development of a software capable of translating provability in deterministic and non-deterministic finite-valued logical systems into operations on polynomial rings. (AU) | |
| FAPESP's process: | 10/51038-0 - Logical consequence, reasoning and computation - LOGCONS |
| Grantee: | Walter Alexandre Carnielli |
| Support Opportunities: | Research Projects - Thematic Grants |