| Texto completo | |
| Autor(es): |
Carnielli, Walter
;
Matulovic, Mariana
Número total de Autores: 2
|
| Tipo de documento: | Artigo Científico |
| Fonte: | ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE; v. 305, p. 16-pg., 2014-07-11. |
| Resumo | |
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) | |
| Processo FAPESP: | 10/51038-0 - Logical consequence, reasoning and computation - LOGCONS |
| Beneficiário: | Walter Alexandre Carnielli |
| Modalidade de apoio: | Auxílio à Pesquisa - Temático |