Approaches to parallel quantifier elimination

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Approaches to parallel quantifier elimination

Full text

Pdf (250 KB)

Source

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

Rostock, Germany

Pages: 88 - 95

Year of Publication: 1998

ISBN:1-58113-002-3

Authors

Andreas Dolzmann	Department of Mathematics and Computer Science, University of Passau, Germany
Oliver Gloor	Institute for Computer Science, University of Tübingen, Germany
Thomas Sturm	Department of Mathematics and Computer Science, University of Passau, Germany

Sponsors

German Comp Soc : GI - Gesellshaft for Informatik
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): 4, Downloads (12 Months): 11, Citation Count: 2

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/281508.281564 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.

	1	Beatrice Amrhein , Oliver Gloor , Wolfgang Küchlin, A case study of multi-threaded Gröbner basis completion, Proceedings of the 1996 international symposium on Symbolic and algebraic computation, p.95-102, July 24-26, 1996, Zurich, Switzerland [doi>10.1145/236869.236908]
	2	Beatrice Amrhein , Oliver Gloor , Wolfgang Küchlin, On the walk, Theoretical Computer Science, v.187 n.1-2, p.179-202, Nov. 15, 1997 [doi>10.1016/S0304-3975(97)00064-9]
	3	BASU~ S.~ POLLACK~ R.~ AND ROY~ M.-F. On the combinatorial and algebraic complexity of quantifier elimination. In Proceedings of the 35th Annual Symposium on Foundations of Computer Science (Los Alamitos~ CA~ USA~ Nov. 1994)~ S. Goldwasser~ Ed.~ IEEE Computer Society Press~ pp. 632-641.
	4	BECKER~ E.~ AND WSRMANN~ T. On the trace formula for quadratic forms. In Recent Advances in Real Algebraic Geometry and Quadratic Forms~ W. B. Jacob~ T.- Y. Lam~ and R. O. Robson~ Eds.~ vol. 155 of Contemporary Mathematics. American Mathematical Society~ Providence~ Rhode Island~ 1994~ pp. 271-291. Proceedings of the RAGSQUAD Year~ Berkeley~ 1990-1991.
	5	Till Bubeck , M. Hiller , Wolfgang Küchlin , Wolfgang Rosenstiel, Distributed Symbolic Computation with DTS, Proceedings of the Second International Workshop on Parallel Algorithms for Irregularly Structured Problems, p.231-248, September 04-06, 1995
	6	BUCHBERGER~ B.~ COLLINS~ G. E.~ ENCARNACION~ M. J.~ HONG~ H.~ JOHNSON~ J. R.~ KRANDICK~ W.~ LOOS~ R.~ MANDACHE~ A. M.~ NEUBACHER~ A.~ AND VIELHABER~ g. Saclib 1.1 user's guide. RISC-Linz Series Technical Report 93-19~ Research Institute for Symbolic Computation~ Johannes Kepler University~ A-4040 Linz~ Austria~ 1993.
	7	George E. Collins, Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, p.134-183, May 20-23, 1975
	8	George E. Collins, The SAC-2 Computer Algebra System, Research Contributions from the European Conference on Computer Algebra-Volume 2, p.34-35, April 01-03, 1985
	9	George E. Collins , Hoon Hong, Partial cylindrical algebraic decomposition for quantifier elimination, Journal of Symbolic Computation, v.12 n.3, p.299-328, Sept. 1991 [doi>10.1016/S0747-7171(08)80152-6]
	10	James H. Davenport , Joos Heintz, Real quantifier elimination is doubly exponential, Journal of Symbolic Computation, v.5 n.1-2, p.29-35, February/April 1988 [doi>10.1016/S0747-7171(88)80004-X]
	11	DOLZMANN, A. Reelle Quantorenelimination durch parametrisches Z/ihlen von Nullstellen. Diploma thesis, Universit/it Passau, D-94030 Passau, Germany, Nov. 1994.
	12	DOLZMANN, A., AND STURM, T. Redlog user manual. Technical Report MIP-9616, FMI, Universit/it Passau, D-94030 Passau, Germany, Oct. 1996. Edition 1.0 for Version 1.0.
	13	Andreas Dolzmann , Thomas Sturn, REDLOG: computer algebra meets computer logic, ACM SIGSAM Bulletin, v.31 n.2, p.2-9, June 1997 [doi>10.1145/261320.261324]
	14	Andreas Dolzmann , Thomas Sturm, Simplification of quantifier-free formulae over ordered fields, Journal of Symbolic Computation, v.24 n.2, p.209-231, August 1997 [doi>10.1006/jsco.1997.0123]
	15	Andreas Dolzmann , Thomas Sturm , Volker Weispfenning, A New Approach for Automatic Theorem Proving in Real Geometry, Journal of Automated Reasoning, v.21 n.3, p.357-380, December 1998 [doi>10.1023/A:1006031329384]
	16	DOLZMANN, A., STURM, T., AND WEISPFENNING, V. Real quantifier elimination in practice. Technical Report MIP-9720, FMI, Universit/it Passau, D-94030 Passau, Germany, Dec. 1997.
	17	GEIST, A., BEGUELIN, A., DONGARRA, J., JIANG, W., MANCHEK, 1~., AND SUNDERAM, V. PVM 3 User's Guide and Reference Manual. Oak Ridge National Laboratory, Oak Ridge, Tennessee 37831, Sept. 1994.
	18	GLOOR, O., AND M/JLLER, S. PARCAN--a parallel computer algebra nucleus. In preparation, 1998.
	19	GONZJ~LEZ-VEGA, L. A combinatorial algorithm solving some quantifier elimination problems. Technical Report 11-1993, University of Cantabria, Departemento de Mathematicas, Estadistica y Computacidn, Facultad de Ciencias, Avenida de Los Castros, 39071 Santander, Spain, Nov. 1993.
	20	HEARN, A. C., AND FITCH, J. P. Reduce User's Manual for Version 3.6. RAND, Santa Monica, CA 90407- 2138, July 1995. RAND Publication CP78.
	21	H. Hong, An improvement of the projection operator in cylindrical algebraic decomposition, Proceedings of the international symposium on Symbolic and algebraic computation, p.261-264, August 20-24, 1990, Tokyo, Japan [doi>10.1145/96877.96943]
	22	Hoon Hong, Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination, Papers from the international symposium on Symbolic and algebraic computation, p.177-188, July 27-29, 1992, Berkeley, California, United States [doi>10.1145/143242.143306]
	23	Hoon Hong, Parallelization of Quantifier Elimination on a Workstation Network, Proceedings of the 10th International Symposium on Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, p.170-179, May 10-14, 1993
	24	Hoon Hong, Quantifier elimination for formulas constrained by quadratic equations, Proceedings of the 1993 international symposium on Symbolic and algebraic computation, p.264-274, July 06-08, 1993, Kiev, Ukraine [doi>10.1145/164081.164140]
	25	HONG, H. Quantifier elimination for formulas constrained by quadratic equations via slope resultants. THE Computer Journal 36, 5 (1993), 440-449. Special issue on computational quantifier elimination.
	26	Hoon Hong , Andreas Neubacher , Wolfgang Schreiner, The design of the SACLIB/PACLIB kernels, Journal of Symbolic Computation, v.19 n.1-3, p.111-132, Jan./Feb./March 1995 [doi>10.1006/jsco.1995.1007]
	27	Wolfgang Kuechlin, PARSAC-2: A Parallel SAC-2 Based on Threads, Proceedings of the 8th International Symposium on Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, p.341-353, August 20-24, 1990
	28	Wolfgang Küchlin, The S-Threads Environment for Parallel Symbolic Computation, Proceedings of the Second International Workshop on Computer Algebra and Parallelism, p.1-18, May 09-11, 1990
	29	K/JCHLIN, W. PARSAC-2: Parallel computer algebra on the desk-top. In Computer Algebra in Science and Engineering (Bielefeld, Germany, Aug. 1994), J. Fleischer, J. Grabmeier, F. Hehl, and W. K/ichlin, Eds., World Scientific, Singapore, 1995, pp. 24-43.
	30	Loos, R., AND WEISPFENNING, V. Applying linear quantifier elimination. The Computer Journal 36, 5 (1993), 450-462. Special issue on computational quantifier elimination.
	31	Scott McCallum, An improved projection operation for cylindrical algebraic decomposition of three-dimensional space, Journal of Symbolic Computation, v.5 n.1-2, p.141-161, February/April 1988 [doi>10.1016/S0747-7171(88)80010-5]
	32	MELENK, H., AND NEUN, W. RR: Parallel symbolic algorithm support for PSL based REDUCE. Preliminary Draft, 1995.
	33	PEDERSEN, P., RoY, M.-F., AND SZPIRGLAS~ A. Counting real zeroes in the multivariate case. In Computational Algebraic Geometry, F. Eysette and A. Galigo, Eds., vol. 109 of Progress in Mathematics. BirkhS~user, Boston, Basel; Berlin, 1993, pp. 203-224. Proceedings of the MEGA 92.
	34	James Renegar, On the computational complexity and geometry of the first-order theory of the reals. Part II: The general decision problem. Preliminaries for quantifier elimination, Journal of Symbolic Computation, v.13 n.3, p.301-327, March 1992
	35	B. D. Saunders , H. R. Lee , S. K. Abdali, A parallel implementation of the cylindrical algebraic decomposition algorithm, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation, p.298-307, July 17-19, 1989, Portland, Oregon, United States [doi>10.1145/74540.74576]
	36	SCHREINER, W., AND HONG, H. A new library for parallel algebraic computation. In Sixth SIAM Conference on Parallel Processing for Scientific Computing (Norfolk, Virginia, Mar. 1993), R. F. Sincovec et al., Eds., vol. 2, SIAM, pp. 776-783.
	37	STURM~ T. Real quadratic quantifier elimination in Risa/Asir. Research Memorandum ISIS-RM-5E, ISIS, Fujitsu Laboratories Limited, 1-9-3, Nakase, Mihamaku, Chiba-shi, Chiba 261, Japan, Sept. 1996.
	38	TARSKI~ A. A decision method for elementary algebra and geometry. Tech. rep., RAND, Santa Monica, CA, 1948.
	39	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]
	40	Volker Weispfenning, Comprehensive Gro¨bner bases, Journal of Symbolic Computation, v.14 n.1, p.1-29, July 1992 [doi>10.1016/0747-7171(92)90023-W]
	41	WEISPFENNING~ V. A new approach to quantifier elimination for real algebra. Tech. Rep. MIP-9305, FMI, UniversitS~t Passau, D-94030 Passau, Germany, July 1993.
	42	Volker Weispfenning, Quantifier elimination for real algebra—the cubic case, Proceedings of the international symposium on Symbolic and algebraic computation, p.258-263, July 20-22, 1994, Oxford, United Kingdom [doi>10.1145/190347.190425]
	43	WEISPFENNING~ V. Quantifier elimination for real algebra--the quadratic case and beyond. Applicable Algebra in Engineering Communication and Computing 8, 2 (Feb. 1997), 85-101.
	44	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]

CITED BY 2

	Andreas Dolzmann , Thomas Sturm, P-adic constraint solving, Proceedings of the 1999 international symposium on Symbolic and algebraic computation, p.151-158, July 28-31, 1999, Vancouver, British Columbia, Canada
	Johannes Grabmeier , Erich Kaltofen , Volker Weispfenning, Cited References, Computer algebra handbook, Springer-Verlag New York, Inc., New York, NY, 2003