zbMATH — the first resource for mathematics

Exploiting data dependencies in many-valued logics. (English) Zbl 0836.03013
Summary: The purpose of this paper is to make some practically relevant results in automated theorem proving available to many-valued logics with suitable modifications. We are working with a notion of many-valued first-order clauses which any finitely-valued logic formula can be translated into and that has been used several times in the literature, but in an ad hoc way. We give a many-valued version of polarity which in turn leads to natural many-valued counterparts of Horn formulas, hyperresolution, and a Davis-Putnam procedure. We show that the many-valued generalizations share many of the desirable properties of the classical versions. Our results justify and generalize several earlier results on theorem proving in many-valued logics.

03B35 Mechanization of proofs and logical operations
03B50 Many-valued logic
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Anderson R., JACM 17 pp 525– (1970) · Zbl 0199.31502 · doi:10.1145/321592.321603
[2] Buro, M. and Büning, H. K. 1992. ”Report on a SAT competition. Reihe Informatik 110, FB 17–Mathematik/Informatik, Universität Paderborn, Nov”. · Zbl 1023.68656
[3] Baaz M., Proc. Logic Programming and Automated Reasoning LPAR’92 pp 107– (1992) · doi:10.1007/BFb0013053
[4] Cohn P. M., Universal Algebra., (1981) · doi:10.1007/978-94-009-8399-1
[5] Dowling W., Journal of Logic Programming 3 pp 267– (1984) · Zbl 0593.68062 · doi:10.1016/0743-1066(84)90014-1
[6] Davis M., Communications of the ACM 5 pp 394– (1962) · Zbl 0217.54002 · doi:10.1145/368273.368557
[7] Escalada Imaz G., Proc. International Symposium on Multiple- Valued Logics, ISMVL’94, Boston/MA, USA pp 250– (1994) · doi:10.1109/ISMVL.1994.302194
[8] Gallo G., Journal of Logic Programmming 7 (1) pp 45– (1989) · Zbl 0672.68044 · doi:10.1016/0743-1066(89)90009-5
[9] Hodges W., Handbook of Logic in Artificial Intelligence and Logic Programming pp 449– (1992)
[10] Hähnle R., Proceedings ISMIS’93, Trondheim, Norway pp 49– (1993)
[11] Hodges W., Encyclopedia of Mathematics and Its Applications. (1993)
[12] Hooker, J. N. 1993. ”Logic-based methods for optimization. A tutorial. Working Paper, GSIA, CMU Pittsburgh, December”.
[13] Hähnle R., Journal of Logic and Computation, to appear (1994)
[14] Jeroslow R. G., Annals of Mathematics and Artificial Intelligence 1 pp 167– (1990) · Zbl 0878.68107 · doi:10.1007/BF01531077
[15] Kowalski R., Machine Intelligence 4 pp 87– (1969)
[16] Lu J. J., Automated Reasoning: Essays in Honor of Woody Bledsoe pp 181– (1991)
[17] Lu J. J., Proc. International Symposium on Multiple-Valued Logics pp 48– (1993)
[18] Lu J. J., Proc. International Conference on Methodologies for Intelligent Systems, ISMIS’94, Charlotte/NC, USA pp 75– (1994)
[19] Murray N. V., Artificial Intelligence 18 pp 67– (1982) · Zbl 0472.68053 · doi:10.1016/0004-3702(82)90011-X
[20] Makowsky J. A., Journal of Computer and System Sciences 34 pp 266– (1987) · Zbl 0619.68029 · doi:10.1016/0022-0000(87)90027-4
[21] Murray N. V., Proceedings ISMIS’93, Trondheim, Norway pp 275– (1993)
[22] Robinson J. A., Int. Journal of Computer Math. 1 pp 227– (1965)
[23] Schmitt R. H., Proc. 8th International Conference on Automated Deduction pp 190– (1986) · doi:10.1007/3-540-16780-3_90
[24] Stachniak Z., Fundamenta Informaticae, XIII:333–351 (1990)
[25] Siekmann J., Automation of Reasoning: Classical Papers in Computational Logic 1957–1966, volume 1. Springer-Verlag (1983)
[26] Siekmann J., Automation of Reasoning: Classical Papers in Computational Logic 1967–1970, volume 2. Springer-Verlag (1983)
[27] Waszkiewicz J., Studia Logica, XXV:7–13 (1969)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.