# zbMATH — the first resource for mathematics

Discriminator varieties and symbolic computation. (English) Zbl 0803.08002
Summary: We look at two aspects of discriminator varieties which could be of considerable interest in symbolic computation:
1. Discriminator varieties are unitary (i.e., there is always a most general unifier of two unifiable terms), and
2. Every mathematical problem can be routinely cast in the form $p_ 1\approx q_ 1,\dots, p_ k\approx q_ k\quad\text{implies the equation } x\approx y.$ Item (1) offers possibilities for implementations in computational logic, and (2) shows that Birkhoff’s five rules of inference for equational logic are all one needs to prove theorems in mathematics.

##### MSC:
 08B05 Equational logic, Mal’tsev conditions 08A70 Applications of universal algebra in computer science 68W30 Symbolic computation and algebraic computation
Full Text:
##### References:
 [1] Ackermann, W., () [2] Albert, M.H.; Lawrence, J., Solving equations in nilpotent groups, (1991), Preprint [3] Arens, R.F.; Kaplansky, I., Topological representations of algebras, Trens. amer. math. soc., 63, 457-481, (1948) · Zbl 0032.00702 [4] Bernays, P.; Bernays, P., A system of axiomatic set theory. part II, J. symbolic logic, J. symbolic logic, 6, 1-17, (1937/1941) · JFM 67.0155.04 [5] Birkhoff, G., On the structure of abstract algebras, Proc. oamb. phil. soc., 31, 433-454, (1935) · Zbl 0013.00105 [6] Birkhoff, G., Subdirect unions in universell algebra, Bull. amer. math. soc., 50, 764-768, (1944) · Zbl 0060.05809 [7] Bloom, S.L.; Tindell, R., Varieties of “if-then-else”, SIAM J. computing, 12, 677-707, (1983) · Zbl 0518.68010 [8] Bulman-Fleming, S.; Werner, H., Equational compactness in quasi-primal varieties, Algebra universalis, 7, 33-46, (1977) · Zbl 0367.08006 [9] Büttner, W.; Simonis, H., Embedding Boolean expressions into logic programming, J. symbolic computation, 4, 191-207, (1987) · Zbl 0641.68148 [10] Burris, S., Boolean constructions, Universal algebra and lattice theory, 1004, 67-90, (1984), Springer Lect. Notes in Math. [11] Burris, S., McKenzie, R., Valeriote, M., Decidable discriminator varieties. To appear in J. Symbolic Logic. · Zbl 0747.08008 [12] Burris, S.; Sankappanavar, H.P., (), Graduate Texts in Math. · Zbl 0478.08001 [13] Burris, S.; Werner, H., Sheaf constructions and their elementary properties, Trans. amer. math. soc., 248, 269-309, (1979) · Zbl 0411.03022 [14] Dauns, J.; Hofmann, K.H., The representation of biregular rings by sheaves, Math. Z., 91, 103-123, (1966) · Zbl 0178.37003 [15] Dershowitz, N., Completion and its applications, () [16] Foster, A.L., Generalized “boolean” theory of universal algebras. part I. subdirect sums and normal representation theorem, Math. Z., 58, 306-336, (1953) · Zbl 0051.02201 [17] Foster, A.L., Generalized “boolean” theory of universal algebras. part II, identities and subdirect sums in functionally complete algebras, Math. Z., 59, 191-199, (1953) · Zbl 0051.26202 [18] Garey, M.R.; Johnson, D.S., () [19] Gödel, K., () [20] Henkln, L.; Monk, D.; Tarski, A.; Henkln, L.; Monk, D.; Tarski, A., Cylindric algebras. part I, Cylindric algebras. part II, (1975/1985), North Holland · Zbl 0576.03043 [21] Herbrand, J., Recherches sur la théorie de la démonstration, Travaux de la société des sciences et des lettres varsovie. cl. III, 33, (1930), 128 pp · JFM 56.0824.02 [22] Herstein, I.N., () [23] Hsiang, J.; Dershowitz, N., Rewrite methods for clausal and non-clausal theorem proving, (), 331-346, Springer-Verlag Lecture Notes in Computer Science · Zbl 0523.68080 [24] Hsiang, J., Refutational theorem proving using term rewriting systems, Artificial intelligence, 25, 255-300, (1985) · Zbl 0558.68072 [25] Hsiang, J., Rewrite method for theorem proving in first-order theory with equality, J. symbolic computation, 3, 133-151, (1987) · Zbl 0637.68104 [26] Huntington, E.V., Sets of independent postulates for the algebra of logic, Trans. amer. math. soc., 5, 288-309, (1904) · JFM 35.0087.02 [27] Jacobson, N., Structure theory for algebraic algebras of bounded degree, Ann. of math., 46, 695-707, (1945) · Zbl 0060.07501 [28] McCoy, N.H.; Montgomery, D., A representation of generalized Boolean rings, Duke math. J., 3, 455-459, (1937) · Zbl 0017.24402 [29] Lawrence, J, A note on the unification of group equations, (1991), Preprint [30] Lawrence, J, Unification in nilpotent and solvable varieties of groups, (1991), Preprint [31] McKenzie, R., On spectra, and the negative solution of the decision problem for identities having a finite non-trivial model, J. symbolic logic, 40, 186-196, (1975) · Zbl 0316.02052 [32] McKenzie, R.; McNulty, G.; Taylor, W., () [33] McNulty, G., An equational logic sampler, (), 234-262, Lecture Notes in Computer Science [34] Mekler, A.H.; Nelson, E.M., Equational bases for if-then-else, SIAM J. computing, 16, 465-485, (1987) · Zbl 0654.68029 [35] Mostowski, A., () [36] Nipkow, T., Unification in primal algebras, their powers and their varieties, J. assoc. comp. Mach., 37, 742-776, (1990) · Zbl 0711.68092 [37] Padmanabhan, R., Equational theory of algebras with a majority polynomial, Algebra universalis, 7, 273-275, (1977) · Zbl 0383.08005 [38] Paul, E., Equational methods in first-order predicate calculus, J. symbolic computation, 1, 7-29, (1985) · Zbl 0577.03003 [39] Robinson, J.A., A machine oriented logic based on the resolution principle, J. assoc. comp. Mach., 12, 23-41, (1965) · Zbl 0139.12303 [40] Rosenbloom, P.O., Post algebras I. postulates and general theory, Amer. J. math., 64, 167-188, (1942) · Zbl 0060.06701 [41] Schröder, E., () [42] Siekmann, J., Unification theory, J. symbolic computation, 7, 207-274, (1989) · Zbl 0678.68098 [43] Tarski, A.; Givant, S., A formalism of set theory without variables, Amer. math. soc. colloq. publications, 41, (1987) · Zbl 0654.03036 [44] Taylor, W., Equational logic, Houston J. of math, 5, (1979) · Zbl 0421.08004 [45] von Neumann, J., Eine axiomatisierung der mengenlehre, J. reine angew. math., 154, 219-240, (1925) · JFM 51.0163.04 [46] Werner, H., (), Studien zur Algebra und ihre Anwendungen
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.