1997, Vol. IV, Núm. 2 "Deduction in many-valued logic" http://hdl.handle.net/2099/2064 2023-05-29T08:51:35Z 2023-05-29T08:51:35Z Editorial [Special issue: Deduction in MVL] Escalada Imaz, Gonzalo Hähnle, Reiner http://hdl.handle.net/2099/3676 2019-01-24T09:30:54Z 2007-10-15T11:24:01Z Editorial [Special issue: Deduction in MVL] Escalada Imaz, Gonzalo; Hähnle, Reiner 2007-10-15T11:24:01Z Escalada Imaz, Gonzalo Hähnle, Reiner Deduction in many-valued logics: a survey Hähnle, Reiner Escalada Imaz, Gonzalo http://hdl.handle.net/2099/3490 2019-01-24T09:30:54Z 2007-09-14T11:53:10Z Deduction in many-valued logics: a survey Hähnle, Reiner; Escalada Imaz, Gonzalo 2007-09-14T11:53:10Z Hähnle, Reiner Escalada Imaz, Gonzalo A reduction-based theorem prover for 3-valued logic Aguilera Venegas, Gabriel Pérez de Guzmán Molina, Inmaculada Ojeda Aciego, Manuel http://hdl.handle.net/2099/3489 2017-02-07T16:04:32Z 2007-09-14T11:46:18Z A reduction-based theorem prover for 3-valued logic Aguilera Venegas, Gabriel; Pérez de Guzmán Molina, Inmaculada; Ojeda Aciego, Manuel 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. 2007-09-14T11:46:18Z Aguilera Venegas, Gabriel Pérez de Guzmán Molina, Inmaculada Ojeda Aciego, Manuel 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. Computing multiple-valued logic programs Lu, James J. Calmet, Jacques Schü, Joachim http://hdl.handle.net/2099/3488 2017-02-07T16:04:32Z 2007-09-14T11:30:34Z Computing multiple-valued logic programs Lu, James J.; Calmet, Jacques; Schü, Joachim The logic of signed formula can be used to reason about a wide variety of multiple-valued logics \cite{hah94,lmr96}. The formal theoretical foundation of multiple-valued logic programming based on signed formulas is set forth in \cite{lu96}. The current paper is an investigation into the operational semantics of such signed logic programming. The connection of signed logic programming to constraint logic programming is presented, search space issues are briefly discussed for both general and special cases, and applications to bilattice logic programming and truth-maintenance are analyzed. 2007-09-14T11:30:34Z Lu, James J. Calmet, Jacques Schü, Joachim The logic of signed formula can be used to reason about a wide variety of multiple-valued logics \cite{hah94,lmr96}. The formal theoretical foundation of multiple-valued logic programming based on signed formulas is set forth in \cite{lu96}. The current paper is an investigation into the operational semantics of such signed logic programming. The connection of signed logic programming to constraint logic programming is presented, search space issues are briefly discussed for both general and special cases, and applications to bilattice logic programming and truth-maintenance are analyzed. Parameterized prime implicant/implicate computations for regular logics Ramesh, Anavi Murray, Neil V. http://hdl.handle.net/2099/3487 2017-02-07T16:04:32Z 2007-09-14T11:08:00Z Parameterized prime implicant/implicate computations for regular logics Ramesh, Anavi; Murray, Neil V. Prime implicant/implicate generating algorithms for multiple-valued logics (MVL's) are introduced. Techniques from classical logic not requiring large normal forms or truth tables are adapted to certain "regular'' multiple-valued logics. This is accomplished by means of signed formulas, a meta-logic for multiple valued logics; the formulas are normalized in a way analogous to negation normal form. The logic of signed formulas is classical in nature. The presented method is based on path dissolution, a strongly complete inference rule. The generalization of dissolution that accommodates signed formulas is described. The method is first characterized as a procedure iterated over the truth value domain $\Delta\,=\,\{0,1, \dots ,n-1\}$ of the MVL. The computational requirements are then reduced via parameterization with respect to the elements and the cardinality of $\Delta$. 2007-09-14T11:08:00Z Ramesh, Anavi Murray, Neil V. Prime implicant/implicate generating algorithms for multiple-valued logics (MVL's) are introduced. Techniques from classical logic not requiring large normal forms or truth tables are adapted to certain "regular'' multiple-valued logics. This is accomplished by means of signed formulas, a meta-logic for multiple valued logics; the formulas are normalized in a way analogous to negation normal form. The logic of signed formulas is classical in nature. The presented method is based on path dissolution, a strongly complete inference rule. The generalization of dissolution that accommodates signed formulas is described. The method is first characterized as a procedure iterated over the truth value domain $\Delta\,=\,\{0,1, \dots ,n-1\}$ of the MVL. The computational requirements are then reduced via parameterization with respect to the elements and the cardinality of $\Delta$.