Mostra el registre d'ítem simple
A reduction-based theorem prover for 3-valued logic
dc.contributor.author | Aguilera Venegas, Gabriel |
dc.contributor.author | Pérez de Guzmán Molina, Inmaculada |
dc.contributor.author | Ojeda Aciego, Manuel |
dc.date.accessioned | 2007-09-14T11:46:18Z |
dc.date.available | 2007-09-14T11:46:18Z |
dc.date.issued | 1997 |
dc.identifier.issn | 1134-5632 |
dc.identifier.uri | http://hdl.handle.net/2099/3489 |
dc.description.abstract | We present a new prover for propositional 3-valued logics, TAS-M3, which is an extension of the TAS-D prover for classical propositional logic. TAS-M3 uses the TAS methodology and, consequently, it is a {\em reduction-based\/} method. Thus, its power is based on the reductions of the size of the formula executed by the $\efe$ transformation. This transformation dynamically "filters" the information contained in the syntactic structure of the formula to avoid as much distributions (of $\land$ wrt $\lor$ in our case) as possible, in order to improve efficiency. In our opinion, this filtering is the key of the TAS methodology which, as shown in this paper, allows the method to be extremely adaptable, because switching to different kinds of logic is possible without having to redesign the whole prover. |
dc.format.extent | 99-127 |
dc.language.iso | eng |
dc.publisher | Universitat Politècnica de Catalunya. Secció de Matemàtiques i Informàtica |
dc.relation.ispartof | Mathware & soft computing . 1997 Vol. 4 Núm. 2 |
dc.rights | Reconeixement-NoComercial-CompartirIgual 3.0 Espanya |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/3.0/es/ |
dc.subject.other | TAS-M3 |
dc.subject.other | TAS-methodology |
dc.subject.other | Reduction based method |
dc.title | A reduction-based theorem prover for 3-valued logic |
dc.type | Article |
dc.subject.lemac | Lògica matemàtica |
dc.subject.ams | Classificació AMS::03 Mathematical logic and foundations::03B General logic |
dc.rights.access | Open Access |
Fitxers d'aquest items
Aquest ítem apareix a les col·leccions següents
-
1997, Vol. IV, Núm. 2 [5]
"Deduction in many-valued logic"