A reduction-based theorem prover for 3-valued logic
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2099/3489
Tipus de documentArticle
Data publicació1997
EditorUniversitat Politècnica de Catalunya. Secció de Matemàtiques i Informàtica
Condicions d'accésAccés obert
Llevat que s'hi indiqui el contrari, els
continguts d'aquesta obra estan subjectes a la llicència de Creative Commons
:
Reconeixement-NoComercial-SenseObraDerivada 3.0 Espanya
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.
ISSN1134-5632
Col·leccions
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
Aguilera.pdf | 449,6Kb | Visualitza/Obre |