Mixed real-integer linear quantifier elimination

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Mixed real-integer linear quantifier elimination

Full text

Pdf (856 KB)

Source

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

Vancouver, British Columbia, Canada

Pages: 129 - 136

Year of Publication: 1999

ISBN:1-58113-073-2

Author

Volker Weispfenning

Fakulatät für Mathematik and 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): 34, Citation Count: 13

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/309831.309888 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	ABDALLAH, C. T., DORATO, P., YANG, W., LISKA, R., AND STEINBERG. S. Applications of quantifier elimination theory to control system design. In Proceedings of the 4 th IEEE Mediterranean Syrnposium on Control and Automation (1996), IEEE, pp. 340-345.
	2	DOLZMANN, A., AND STURM, T. Redlog User Manual. FMI, Universit~t Passau, D-94030 Passau, Germany: Oct. 1996. Edition 1.0 for Version 1.0.
	3	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]
	4	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]
	5	DOLZMANN, A., STURM, T., AND WEISPFENNING, V. Real quantifier elimination in practice. In Algorithmic Algebra and Number Theory, B. H. Matzat, G.- M. Greuel, and G. Hiss, Eds. Springer, Berlin, 1998, pp. 221-247.
	6	Peter Dorato , Wei Yang , Chaouki Abdallah, Robust multi-objective feedback design by quantifier elimination, Journal of Symbolic Computation, v.24 n.2, p.153-159, August 1997 [doi>10.1006/jsco.1997.0120]
	7	DRIES, L. v. D. Tame Topology and o-minimal structures. Cambridge University Press, 1998.
	8	Mats Jirstrand, Nonlinear control system design by quantifier elimination, Journal of Symbolic Computation, v.24 n.2, p.137-152, August 1997 [doi>10.1006/jsco.1997.0119]
	9	K~PPL, C. Eine REDUCE-Implementierung eines Quantoreneliminationsverfahrens f~r die Presburger Arithmetik. Master's thesis, Universit~t Passau, Universit~t Passau, FMI, 1991.
	10	LAFFERRIERE, G., PAPPAS, G. J., AND YOVlNE, S. Decidable hybrid systems. Tech. rep., VERIMAG, Univ. of Grenoble, 1998.
	11	LIPSIIITZ, L. The diophantine problem for addition and divisibility. Trans. AMS 235 (1978), 271-283.
	12	Loos, R., AND WEISPEENNlNG, V. Applying linear quantifier elimination. The Computer Journal ,36, 5 (1993), 450-462. Special issue on computational quantifier elimination.
	13	PRESBURGER, M. ~ber die Vollst~ndigkeit eines gewissen Systems der Arithmetik. In Comptes rendues du 1 er Congres des Mathematique des Pays Slaves (Warsaw, 1929), vol. 395, pp. 92 101.
	14	STURM, T., AND WEISPFENNING, V. Rounding and blending of solids by a real elimination method. In Proceedings of the 15th IMACS World Congress on Scientific Computation, Modelling, and Applied Mathematics (IMACS 97) (Berlin, Aug. 1997), A. Sydow, Ed., vol. 2, IMACS, Wissenschaft & Technik Verlag, pp. 727--732.
	15	Thomas Sturm , Volker Weispfenning, Computational Geometry Problems in REDLOG, Selected Papers from the International Workshop on Automated Deduction in Geometry, p.58-86, September 27-29, 1996
	16	TARSKI. A. A decision method for elementary algebra and geometry. Tech. rep., RAND, Santa Monica, CA, 1948.
	17	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]
	18	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]
	19	Volker Weispfenning, Complexity and uniformity of elimination in Presburger arithmetic, Proceedings of the 1997 international symposium on Symbolic and algebraic computation, p.48-53, July 21-23, 1997, Kihei, Maui, Hawaii, United States [doi>10.1145/258726.258746]
	20	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]
	21	WEISPFENNING, V. A new approach to quantifier elimination for real algebra. In Quantifier Elimination and Cylindrical Algebraic Decomposition. B. Caviness and J. Johnson, Eds., Texts and Monographs in Symbolic Computation. Springer, Wien, New York, 1998, pp. 376-392.
	22	WEISPFENNING. V., AND XUE. R. Parametric mixed integer programming by elimination. Technical Report. MIP-9503, Universit~t Passau, 1995. Poster presentation at ISSAC'95, Montreal.

CITED BY 13

	Hirokazu Anai , Volker Weispfenning, Deciding linear-trigonometric problems, Proceedings of the 2000 international symposium on Symbolic and algebraic computation, p.14-22, July 2000, St. Andrews, Scotland
	Johannes Grabmeier , Erich Kaltofen , Volker Weispfenning, Cited References, Computer algebra handbook, Springer-Verlag New York, Inc., New York, NY, 2003
	Ruggero Lanotte , Andrea Maggiolo-Schettini , Simone Tini, Information flow in hybrid systems, ACM Transactions on Embedded Computing Systems (TECS), v.3 n.4, p.760-799, November 2004
	Bernard Boigelot , Sébastien Jodogne , Pierre Wolper, An effective decision procedure for linear arithmetic over the integers and reals, ACM Transactions on Computational Logic (TOCL), v.6 n.3, p.614-633, July 2005
	Gregor Snelting , Torsten Robschink , Jens Krinke, Efficient path conditions in dependence graphs for software safety analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.15 n.4, p.410-457, October 2006
	Volker Weispfenning, Deciding linear-exponential problems, ACM SIGSAM Bulletin, v.34 n.1, p.30-31, March 2000
	Anatol Slissenko, A Logic Framework for Verification of Timed Algorithms, Fundamenta Informaticae, v.62 n.1, p.29-67, January 2004
	Véronique Bruyère , Emmanuel Dall'olio , Jean-François Raskin, Durations and parametric model-checking in timed automata, ACM Transactions on Computational Logic (TOCL), v.9 n.2, p.1-23, March 2008
	Felix Klaedtke, Bounds on the automata size for Presburger arithmetic, ACM Transactions on Computational Logic (TOCL), v.9 n.2, p.1-34, March 2008
	Jochen Eisinger , Felix Klaedtke, Don't care words with an application to the automata-based approach for real addition, Formal Methods in System Design, v.33 n.1-3, p.85-115, December 2008
	Amine Chaieb , Tobias Nipkow, Proof Synthesis and Reflection for Linear Arithmetic, Journal of Automated Reasoning, v.41 n.1, p.33-59, July 2008
	Ruggero Lanotte, Expressive power of hybrid systems with real variables, integer variables and arrays, Journal of Automata, Languages and Combinatorics, v.12 n.3, p.373-405, January 2007
	Robert Vajda , Tudor Jebelean , Bruno Buchberger, Combining logical and algebraic techniques for natural style proving in elementary analysis, Mathematics and Computers in Simulation, v.79 n.8, p.2310-2316, April, 2009