Ir al contenido

Documat


A reduction-based theorem prover for 3-valued logic

  • Autores: Gabriel Aguilera Venegas Árbol académico, Inmaculada Pérez de Guzmán Molina Árbol académico, Manuel Ojeda Aciego Árbol académico
  • Localización: Mathware & soft computing: The Magazine of the European Society for Fuzzy Logic and Technology, ISSN-e 1134-5632, Vol. 4, Nº. 2, 1997, págs. 99-127
  • Idioma: inglés
  • Títulos paralelos:
    • Demostrador de teoremas, basado en la reducción, para lógica trivaluada
  • Enlaces
  • Resumen
    • 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 reduction-based method. Thus, its power is based on the reductions of the size of the formula executed by the F transformation. This transformation dynamically filters the information contained in the syntactic structure of the formula to avoid as much distributions 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.


Fundación Dialnet

Mi Documat

Opciones de artículo

Opciones de compartir

Opciones de entorno