1997, Vol. IV, Núm. 2"Deduction in many-valued logic"http://hdl.handle.net/2099/20642024-07-18T20:35:38Z2024-07-18T20:35:38ZEditorial [Special issue: Deduction in MVL]Escalada Imaz, GonzaloHähnle, Reinerhttp://hdl.handle.net/2099/36762019-01-24T09:30:54Z2007-10-15T11:24:01ZEditorial [Special issue: Deduction in MVL]
Escalada Imaz, Gonzalo; Hähnle, Reiner
2007-10-15T11:24:01ZEscalada Imaz, GonzaloHähnle, ReinerDeduction in many-valued logics: a surveyHähnle, ReinerEscalada Imaz, Gonzalohttp://hdl.handle.net/2099/34902019-01-24T09:30:54Z2007-09-14T11:53:10ZDeduction in many-valued logics: a survey
Hähnle, Reiner; Escalada Imaz, Gonzalo
2007-09-14T11:53:10ZHähnle, ReinerEscalada Imaz, GonzaloA reduction-based theorem prover for 3-valued logicAguilera Venegas, GabrielPérez de Guzmán Molina, InmaculadaOjeda Aciego, Manuelhttp://hdl.handle.net/2099/34892017-02-07T16:04:32Z2007-09-14T11:46:18ZA 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:18ZAguilera Venegas, GabrielPérez de Guzmán Molina, InmaculadaOjeda Aciego, ManuelWe 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 programsLu, James J.Calmet, JacquesSchü, Joachimhttp://hdl.handle.net/2099/34882017-02-07T16:04:32Z2007-09-14T11:30:34ZComputing 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:34ZLu, James J.Calmet, JacquesSchü, JoachimThe 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 logicsRamesh, AnaviMurray, Neil V.http://hdl.handle.net/2099/34872017-02-07T16:04:32Z2007-09-14T11:08:00ZParameterized 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:00ZRamesh, AnaviMurray, 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$.