zbMATH — the first resource for mathematics

A normal form for restricted exponential functions. (English) Zbl 0665.03018
A first order theory G is defined, the terms of which, roughly speaking, can be built as linear combination of “towers of simple exponentiations” with polynomial coefficients. A term rewriting system \({\mathfrak R}\) is introduced, which converts every term of G to its normal form. \({\mathfrak R}\) can be run as it is on a computer in order to solve the identity problem for a subsystem of \(E=<N_+,+,\times,\exp,1>.\) This is done by showing that two terms in G are identical if and only if they have the same normal form with respect to \({\mathfrak R}\).
03C05 Equational classes, universal algebra in model theory
68Q65 Abstract data types; algebraic specification
08B05 Equational logic, Mal’tsev conditions
03C07 Basic properties of first-order languages and structures
Full Text: DOI EuDML
[1] 1. G. H. HARDY, Orders of infinity, Cambridge Tracts in Math. Phys., 12, Cambridge University Press 1910, Reprint Hafner, New York. JFM41.0303.01 · JFM 41.0303.01
[2] 2. C. W. HENSON and L. A. RUBEL, Some Applications of Nevalinna Theory to Mathematical Logic: Identities of Exponential Functions, Trans. of the American Math. Soc., Vol. 282, No. 1, 1984, pp. 1-32. Zbl0533.03015 MR728700 · Zbl 0533.03015
[3] 3. G. HUET and D. C. OPPEN, Equations and Rewrite Rules: A Survey. In: Formal Languages Theory: Perspectives and Open Problems, R. BOOK Ed., Academic Press, New York, 1980, pp. 349-405.
[4] 4. D. LANKFORD, On Proving Term Rewriting Systems are Noetherian, Rep. MTP-3, Louisiana Tech. Univ., 1979.
[5] 5. H. LEVITZ, An Ordered Set of Arithmetic Functions Representing the Least \epsilon -Number, Z. Math. Logik Grundlag. Math., Vol. 21, 1975, pp. 115-120. Zbl0325.04002 MR371627 · Zbl 0325.04002
[6] 6. A. MACINTYRE, The Laws of Exponentiation. In: Model Theory and Arithmetic, C. BERLINE, K. MCALOON and J.-P. RESSAYRE Eds., Lecture Notes in Mathematics, No. 890, Springer-Verlag, Berlin, 1981, pp. 185-197. Zbl0503.08008 MR645003 · Zbl 0503.08008
[7] 7. C. MARTIN, Equational Theories of Natural Numbers and Transfinite Ordinals, Ph. D. Thesis, Univ. of California, Berkley, 1973.
[8] 8. G. E. PETERSON and M. E. STICKEL, Complete Sets of Reductions for Some Equational Theories, J. of the A.C.M., Vol. 28, 1981, pp. 233-264. Zbl0479.68092 MR612079 · Zbl 0479.68092
[9] 9. A. TARSKI, Equational Logic and Equational Theories of Algebras. In: Contributions to Mathematical Logic, H. A. SCHMIDT, K. SHUTTE and H. J. THIELE Eds., North-Holland, Amsterdam, 1968, pp. 275-288. Zbl0209.01402 MR237410 · Zbl 0209.01402
[10] 10. A. J. WILKIE, On Exponentiation - A Solution to Tarskfs High School Algebra Problem. Unpublished Manuscript, quoted in Assoc. of Automated Reasoning Newsletter, Vol. 3, 1984, p. 6.
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.