Abstract
We investigate the problem of finding optimal axiomatizations for operators and distribution quantifiers in finitely-valued first-order logics. We show that the problem can be viewed as the minimization of certain two-valued prepositional formulas. We outline a general procedure leading to optimized quantifier rules for the sequent calculus, for natural deduction and for clause formation. In the case of operators and quantifiers based on semi-lattices, rules with a minimal branching degree can be obtained by instantiating a schema, which can also be used for optimal tableaux with sets-as-signs.
Supported by FWF grant P10282-MAT.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Baaz and C. G. Fermüller. Resolution-based theorem proving for many-valued logics. J. Symbolic Computation, 19:353–391, 1995.
M. Baaz, C. G. Fermüller, G. Salzer, and R. Zach. MUltlog 1.0: Towards an expert system for many-valued logics. In 13th Int. Conf. on Automated Deduction (CADE'96), LNCS (LNAI). Springer, 1996.
M. Baaz, C. G. Fermüller, and R. Zach. Systematic construction of natural deduction systems for many-valued logics. In Proc. 23rd International Symposium on Multiple-valued Logic, pages 208–215. IEEE Computer Society Press, Los Alamitos, May 24–27 1993.
W. A. Carnielli. Systematization of finite many-valued logics through the method of tableaux. J. Symbolic Logic, 52(2):473–493, 1987.
R. Hähnle. Automated Deduction in Multiple-valued Logics. Clarendon Press, Oxford, 1993.
R. Hähnle. Commodious axiomatization of quantifiers in multiple-valued logic. In Proc. 26th Int. Symp. on Multiple-Valued Logics, Santiago de Compostela, Spain. IEEE Press, Los Alamitos, May 1996.
McCluskey. Minimization of boolean functions. Bell Syst. Techn. J., 35:1417–1444, 1956.
A. Mostowski. On a generalization of quantifiers. Fund. Math., 44:12–36, 1957.
K. F. Nutz. Digitaltechnik, BASIC: Berechnung und Optimierung von Digitalschaltungen mit Hilfe von BASIC-Programmen. Oldenburg, 1984.
W. V. Quine. The problem of simplifying truth functions. American Mathematical Monthly, 59:521–531, 1952.
J. B. Rosser and A. R. Turquette. Many-Valued Logics. North-Holland, Amsterdam, 1952.
G. Rousseau. Sequents in many valued logic I. Fund. Math., 60:23–33, 1967.
N. Zabel. Nouvelles Techniques de Déduction Automatique en Logiques Polyvalentes Finies et Infinies du Premier Ordre. PhD thesis, Institut National Polytechnique de Grenoble, 1993.
R. Zach. Proof Theory of Finite-valued Logics. Diplomarbeit, Technische Universität Wien, 1993.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Salzer, G. (1996). Optimal axiomatizations for multiple-valued operators and quantifiers based on semi-lattices. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_122
Download citation
DOI: https://doi.org/10.1007/3-540-61511-3_122
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61511-8
Online ISBN: 978-3-540-68687-3
eBook Packages: Springer Book Archive