Abstract
We present a transformation of formulae from arbitrary finitely-valued logics into a conjunctive normal form based on signed atomic formulae which can be used to syntactically characterize many-valued validity with a simple resolution rule very much like in classical logic. The transformation is always linear with relation to the size of the input, and we define a generalized concept of polarity in order to remove clauses which are not needed in the proof. The transformation rules are based on the concept of ’sets-as-signs’ developed earlier by the author in the context of tableau-based deduction in many-valued logics. We claim that the approach presented here is much more efficient than existing approaches to many-valued resolution.
Research supported by Deutsche Forschungsgemeinschaft (DFG).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Baaz and C. G. Fermüller. Resolution for many-valued logics. In Proc. LPAR'92, pp. 107–118. Springer, LNAI 624, 1992.
T. Boy de la Tour. Minimizing the number of clauses by renaming. In Proc. 10 th CADE, Kaiserslautern, pp. 558–572. Springer, Heidelberg, July 1990.
R. Hähnle. Towards an efficient tableau proof procedure for multiple-valued logics. In Proc. Workshop Computer Science Logic, Heidelberg, pp. 248–260. Springer, LNCS 533, 1990.
R. Hähnle. Uniform notation of tableaux rules for multiple-valued logics. In Proc. 20 th 1SMVL, Victoria, pp. 238–245. IEEE Press, 1991.
R. Hähnle and W. Kernig. Verification of switch-level circuits with multiple-valued logics. To appear, 1993.
J. J. Lu, L. J. Henschen, V.S. Subrahmanian, and N. C. A. da Costa. Reasoning in paraconsistent logics. In Automated Reasoning: Essays in Honor of Woody Bledsoe, pp. 181–210. Kluwer, 1991.
G. Mints. Gentzen-type systems and resolution rules, part 1: Prepositional logic. In Proc. COLOG-88, Tallin, pp. 198–231. Springer, LNCS 417, 1990.
D. Mundici. Normal forms in infinite-valued logic: The case of one variable. In Proc. Workshop Computer Science Logic 91, Berne. Springer, LNCS, 1991.
N. Murray and E. Rosenthal. Resolution and path-dissolution in multiple-valued logics. In Proc. ISMIS, Charlotte, 1991.
N. V. Murray. Completely non-clausal theorem proving. AI, 18:67–85, 1982.
P. O'Hearn and Z. Stachniak. A resolution framework for finitely-valued first-order logics. Journal of Symbolic Computing, 13:235–254, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hähnle, R. (1993). Short CNF in finitely-valued logics. In: Komorowski, J., Raś, Z.W. (eds) Methodologies for Intelligent Systems. ISMIS 1993. Lecture Notes in Computer Science, vol 689. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56804-2_5
Download citation
DOI: https://doi.org/10.1007/3-540-56804-2_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56804-9
Online ISBN: 978-3-540-47750-1
eBook Packages: Springer Book Archive