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

• Volume: 4, Issue: 2, page 99-127
• ISSN: 1134-5632

top

## Abstract

top
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.

## How to cite

top

Aguilera Venegas, Gabriel, Pérez de Guzmán, Inmaculada, and Ojeda Aciego, Manuel. "A reduction-based theorem prover for 3-valued logic.." Mathware and Soft Computing 4.2 (1997): 99-127. <http://eudml.org/doc/39103>.

@article{AguileraVenegas1997,
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 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.},
author = {Aguilera Venegas, Gabriel, Pérez de Guzmán, Inmaculada, Ojeda Aciego, Manuel},
journal = {Mathware and Soft Computing},
keywords = {Lógica multivaluada; Lógica simbólica; Pruebas; Teoremas; Simplificación; Flexibilidad; many-valued theorem proving; Łukasiewicz logic; propositional three-valued logic; algorithm},
language = {eng},
number = {2},
pages = {99-127},
title = {A reduction-based theorem prover for 3-valued logic.},
url = {http://eudml.org/doc/39103},
volume = {4},
year = {1997},
}

TY - JOUR
AU - Aguilera Venegas, Gabriel
AU - Pérez de Guzmán, Inmaculada
AU - Ojeda Aciego, Manuel
TI - A reduction-based theorem prover for 3-valued logic.
JO - Mathware and Soft Computing
PY - 1997
VL - 4
IS - 2
SP - 99
EP - 127
AB - 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.
LA - eng
KW - Lógica multivaluada; Lógica simbólica; Pruebas; Teoremas; Simplificación; Flexibilidad; many-valued theorem proving; Łukasiewicz logic; propositional three-valued logic; algorithm
UR - http://eudml.org/doc/39103
ER -

## NotesEmbed?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.