Complexity and uniformity of elimination in Presburger arithmetic

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Complexity and uniformity of elimination in Presburger arithmetic

Full text

Pdf (867 KB)

Source

International Conference on Symbolic and Algebraic Computation archive
Proceedings of the 1997 international symposium on Symbolic and algebraic computation table of contents

Kihei, Maui, Hawaii, United States

Pages: 48 - 53

Year of Publication: 1997

ISBN:0-89791-875-4

Author

Volker Weispfenning

Fakultät für Mathematik und Informatik, Universität Passau, D-94030 Passau, Germany

Sponsors

SIGSAM: ACM Special Interest Group on Symbolic and Algebraic Manipulation
SIGNUM: ACM Special Interest Group on Numerical Mathematics

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 24, Citation Count: 4

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/258726.258746 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	Bar68	E.H. Bareiss, Sylvester's identity and multistep integer preserving gaussian elimination, math. of Computation 22, 565-578 (1968).
	Ber77	L. Berman, Precise bounds for Presburger arithmetic and the reals with addition, IEEE Syrup. FOCS 18, 95-99 (1977).
	Ber80	L. Berman, The complexity of logical theories, Th. Comp. Sci. 11, 71-77 (1980).
	Coo72	D.C. Cooper, Theorem-proving in arithmetic without multiplication, Machine Intelligence Vol.7, 91-100 (1972).
	DS96	A. Dolzmann, T. Sturm, rtEDLOC, Computer algebra meets computer logic, preprint MIP-9603, Universit~it Passau (1996).
	DH92	L. van den Dries, J. Holly, Quantifier elimination for modules with scalar variables, Annals of Pure and Applied Logic, 57, 161-179 (1992).
	75	J. Ferrante, Ch. Rackoff, A Decision Procedure for the first Order Theory of Real Addition with Order, SIAM J. Comp. 4, 69-77 (1975).
	79	J. Fcrrante, Ch. Rackoff, The computational complexity of logical theories, Springer Lecture Notes ill Mathmatics, 718 (1979).
	fiR74	M.J. Fischer, M. Rabin, Super-exponential complexity of Presburger arithmetic, SIAM-AMS Proceedings 7, 27-41 (1974).
	f82	M. Fiirer, The complexity of Presburger arithmetic with bounded quantifier alternation depth, Theor. Comp. Sci. 18, 105-111 (1982).
	GS78	J. wm zur Gathen, M. Sieveking, A bound on solutions of linear integer equations and inequalities, Proc. AMS 72, 155-158 (1978).
	G87	E. Graedel, The complexity of subclasses of logical theories, Doctoral Dissertation, Basel (1987).
	G85	Eitan M. Gurari, Decidable problems for powerful programs, Journal of the ACM (JACM), v.32 n.2, p.466-483, April 1985 [doi>10.1145/3149.3157]
	GI79	Eitan M. Gurari , Oscar H. Ibarra, An NP-Complete Number-Theoretic Problem, Journal of the ACM (JACM), v.26 n.3, p.567-581, july 1979 [doi>10.1145/322139.322152]
	GI81	E.M. Gurari, O.H. Ibarra, The complexity of the equivalence problem for two characterizations of Presburger sets Theor. Comp. Science 13, 295- 314 (1981).
	K91	Ch. KSppl. Eine aEDUCE-Implementierung eines Quantoreneliminationsverfahrens f/Jr die Presburger Arithmetik,Diploma Thesis, Universitiit Passau ( 1991 ).
	L93	Christian Lengauer, Loop Parallelization in the Polytope Model, Proceedings of the 4th International Conference on Concurrency Theory, p.398-416, August 23-26, 1993
	L78	L. Lipshitz, The Diophantine problem for addition and divisibility, Trans. AMS 235, 271-283 (1978).
	O73	Derek C. Oppen, Elementary bounds for presburger arithmetic, Proceedings of the fifth annual ACM symposium on Theory of computing, p.34-37, April 30-May 02, 1973, Austin, Texas, United States [doi>10.1145/800125.804033]
	P29	M. Presburger, LIber die VollstRndigkeit eines gewissen Systems der Arithmetik..., Comptes rendues du premier Congres des Math. des Pays Slaves, Warsaw, 92-101,395 (1929).
	RL78	C. R. Reddy , D. W. Loveland, Presburger arithmetic with bounded quantifier alternation, Proceedings of the tenth annual ACM symposium on Theory of computing, p.320-325, May 01-03, 1978, San Diego, California, United States [doi>10.1145/800133.804361]
	Sc84	g. Scarpellini, Complexity of subcases of Presburger arithmetic, Trans. AMS 284, 203-218 (1984).
	Sh77	Robert E. Shostak, On the SUP-INF Method for Proving Presburger Formulas, Journal of the ACM (JACM), v.24 n.4, p.529-543, Oct. 1977 [doi>10.1145/322033.322034]
	SJ80	Norihisa Suzuki , David Jefferson, Verification Decidability of Presburger Array Programs, Journal of the ACM (JACM), v.27 n.1, p.191-205, Jan. 1980 [doi>10.1145/322169.322185]
	V83	H. Volger, Turing machines with linear alternation, theories of bounded concatenation and the decision problem of First Order Theories, Theor. Comp. Sci. 23, 333-337 (1983).
	W88	Volker Weispfenning, The complexity of linear problems in fields, Journal of Symbolic Computation, v.5 n.1-2, p.3-27, February/April 1988 [doi>10.1016/S0747-7171(88)80003-8]
	W90	V. Weispfenning, The complexity of almost linear diophantine problems, Journal of Symbolic Computation, v.10 n.5, p.395-403, Nov. 1990 [doi>10.1016/S0747-7171(08)80051-X]
	W97	Volker Weispfenning, Simulation and optimization by quantifier elimination, Journal of Symbolic Computation, v.24 n.2, p.189-208, August 1997 [doi>10.1006/jsco.1997.0122]
	W97a	V. Weispfenning, Parametric linear, quadratic and hyperbolic optimization by elimination, J. Symb. Comput. to appear, (1997).
	WX95	V. Weispfenning, Xue Rui, Parametric mixed integer programming by elimination, Tech. Report MIP-9503, Universitiit Pa-ssau (1995), poster presentation at ISSAC'95, Montreal.

CITED BY 4

	Volker Weispfenning, Mixed real-integre linear quantifier elimination, Proceedings of the 1999 international symposium on Symbolic and algebraic computation, p.129-136, July 28-31, 1999, Vancouver, British Columbia, Canada
	Siddhartha Chatterjee , Erin Parker , Philip J. Hanlon , Alvin R. Lebeck, Exact analysis of the cache behavior of nested loops, ACM SIGPLAN Notices, v.36 n.5, p.286-297, May 2001
	Jeremy Avigad , Yimu Yin, Quantifier elimination for the reals with a predicate for the powers of two, Theoretical Computer Science, v.370 n.1-3, p.48-59, February, 2007
	Amine Chaieb , Tobias Nipkow, Proof Synthesis and Reflection for Linear Arithmetic, Journal of Automated Reasoning, v.41 n.1, p.33-59, July 2008