Abstract
We find uniform, efficient decision and quantifier elimination procedures for the theory T' of existentially closed models of a locally finite universal theory T, whose class of models has the amalgamation property. Upper bounds on the complexity of these procedures are obtained in terms of the size of n-generated T-models. Applications include the theories T of linear and partial orders, graphs, semilattices, boolean algebras, Stone algebras, distributive p-algebras in general and in the Lee class \(\mathbb{B}_2\), abelian m-groups, and m-rings for a fixed positive integer m.
Preview
Unable to display preview. Download preview PDF.
References
L. Berman 1980, The complexity of logical theories, Theor.Comp.Sci. 11, 71–77.
M. Boffa, G. Cherlin 1980, Elimination des quantificateurs dans les faisceaux, C.R. Acad. Sc. Paris 290, 355–357.
M. Boffa, A. Macintyre, F. Point 1980, The quantifier elimination problem for rings without nilpotent elements and for semisimple rings, Model Theory of Algebra and Arithmetic, Proc. Karpacz, Springer LNM vol. 834, 20–30.
S. Burris 1984, Model companions for finitely generated universal Horn classes, J. Symb. Logic 49, 68–74.
P. Erdös, J. Spencer 1974, Probabilistic methods in Combinatorics, Acad. Press, New York and London.
J. Ferrante, J.R. Geiser 1977, An efficient decision procedure for the theory of rational order, Theor. Comp. Sci. 4, 227–233.
J.Ferrante, C.Rackoff 1979, The computational complexity of logical theories, Springer LNM vol. 718.
G. Grätzer 1971, Lattice theory, Freeman, San Francisco.
D. Kozen 1980, Complexity of boolean algebras, Theor.Comp.Sci. 10, 221–247.
A. Macintyre 1977, Model completeness, in Handbook of Math. Logic, J. Barwise Ed., North-Holland, Amsterdam, 139–180.
R.S.Pierce 1967, Modules over commutative regular rings, AMS Memoirs, vol. 70.
S. Rauschning 1984, Quantifier elimination for Stone algebras, Diplomarbeit, University of Heidelberg.
J. Schmid 1982, Model companions of distributive p-algebras, J. Symb. Logic 42, 680–688.
P. Schmitt 1976, The model completion of Stone algebras, Ann.Sci.Univ.Clermont Math. 13, 135–155.
V. Weispfenning 1975, Model-completeness and elimination of quantifiers for subdirect products of structures, J. of Algebra 36, 252–277.
— " — 1978, A note on aleph-O-categorical model companions, Archiv f. math. Logik 19, 23–29.
— " — 1978', Model theory of lattice products, Habilitationsschrift, University of Heidelberg.
— " — 1983, Aspects of quantifier elimination in algebra, Proc. 25. Arbeitstagung on Universal Algebra, Darmstadt 1983, Heldermann Verlag, Berlin, 85–105.
— " — a, Existentially closed semilattices, Algebra Universalis, to appear.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Weispfenning, V. (1986). Efficient decision algorithms for locally finite theories. In: Calmet, J. (eds) Algebraic Algorithms and Error-Correcting Codes. AAECC 1985. Lecture Notes in Computer Science, vol 229. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16776-5_729
Download citation
DOI: https://doi.org/10.1007/3-540-16776-5_729
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16776-1
Online ISBN: 978-3-540-39855-4
eBook Packages: Springer Book Archive