Presentación | Participantes | Bibliografía (DML-E) | Bibliografía adicional | Enlaces de interés | Otros proyectos DML | Ayuda  
INICIO | 28 de mayo de 2024
  

A reduction-based theorem prover for 3-valued logic.

Título inglés A reduction-based theorem prover for 3-valued logic.
Título español Demostrador de teoremas, basado en la reducción, para lógica trivaluada.
Autor/es Aguilera Venegas, Gabriel ; Pérez de Guzmán, Inmaculada ; Ojeda Aciego, Manuel
Organización Dep. Mat. Apl. Fac. Cienc. Univ. Málaga, Málaga, España
Revista 1134-5632
Publicación 1997, 4 (2): 99-127, 12 Ref.
Tipo de documento articulo
Idioma Inglés
Resumen inglés 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.
Clasificación UNESCO 110214
Palabras clave español Lógica multivaluada ; Lógica simbólica ; Pruebas ; Teoremas ; Simplificación ; Flexibilidad
Código MathReviews MR1621906
Código Z-Math Zbl 0884.03006
Icono pdf Acceso al artículo completo
Equipo DML-E
Instituto de Ciencias Matemáticas (ICMAT - CSIC)
rmm()icmat.es