Article

Free access

Quantifier elimination for formulas constrained by quadratic equations

Author:

Hoon HongAuthors Info & Claims

ISSAC '93: Proceedings of the 1993 international symposium on Symbolic and algebraic computation

Pages 264 - 274

https://doi.org/10.1145/164081.164140

Published: 01 August 1993 Publication History

PDF eReader

References

[1]

D. S. Arnon. Algorithms for the geometry of semialgebraic sets. Technical Report 436, Computer Sciences Dept, Univ. of Wisconsin-Madison, 1981. Ph.D. Thesis.

Digital Library

Google Scholar

[2]

M. Ben-Or, D. Kozen, and J. H. Reif. The complexity of elementary algebra and geometry. J. Cornput. System Sci., 32(2):251-264, 1986.

Digital Library

Google Scholar

[3]

G. E. Collins. Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In Lecture Notes In Computer Science, pages 134-183. Springer-Verlag, Berlin, 1975. Vol. 33.

Digital Library

Google Scholar

[4]

A. Colmerauer. An Introduction to Prolog III. Communications of the A CM, 33(7):69-90, July 1990.

Digital Library

Google Scholar

[5]

N. Fitchas, A. Galligo, and J. Morgenstern. Precise sequential and parallel complexity bounds for quantifier elimination over algebraically closed" fields. Journal of Pure and Applied Algebra, (67):1- 14, 1990.

Google Scholar

[6]

D. Yu. Grigor'ev. The complexity of deciding Tarski algebra. Journal of Symbolic Computation, 5(1,2):65-108, 1988.

Digital Library

Google Scholar

[7]

J. Heintz, M-F. Roy, and P. SolernS. On the complexity of semialgebraic sets. In Proc. IFIP, pages 293-298, 1989.

Google Scholar

[8]

H. Hong. Improvements in CAD-based Quanlifier Elimination. PhD thesis, The Ohio State University, 1990.

Digital Library

Google Scholar

[9]

H. Hong. Comparison of several decision algorithms for the existential theory of the reals. Technical Report 91-41.0, Research Institute for Symbolic Computation, Johannes Kepler University A- 4040 Linz, Austria, 1991.

Google Scholar

[10]

H. Hong. Half resultant. Technical Report 92- 51, Research Institute for Symbolic Computation, Johannes Kepler University A-4040 Linz, Austria, 1992.

Google Scholar

[11]

H. Hong. Non-linear real constraints in constraint logic programming. In international Conference on Algebraic and Logic Programming, pages 201-212, 1992.

Digital Library

Google Scholar

[12]

It. Hong. Slope resultant. Technical Report 92- 52, Research Institute for Symbolic Computation, johannes Kepler University A-4040 Linz, Austria, 1992.

Google Scholar

[13]

joxan jaffar and Jean-Louis Lassez. Constraint logic programming. In Proceedings of the 14th A CM Symposium on Principles of Programming Languages, Munich, Germany, pages 111-119. ACM, January 1987.

Digital Library

Google Scholar

[14]

R. Loos and V. Weispfenning. Applying linear quantifier elimination. Manuscript in preparation, 1992.

Google Scholar

[15]

S. McCallum. An Improved Projection Operator for Cylindrical Algebraic Decomposition. PhD thesis, University of Wisconsin-Madison, 1984.

Digital Library

Google Scholar

[16]

:i. Renegar. On the computational complexity and geometry of the first-order theory of the reals (part III). Technical Report 856, Cornell University, Ithaca, New York 14853-7501 USA, August 1989.

Google Scholar

[17]

A. Tarski. A Decision Method for Elementary Algebra and Geometry. Univ. of California Press, Berkeley, second edition, 1951.

Google Scholar

[18]

V. Weispfenning. The complexity of linear problems in fields. Journal of Symbolic Computation, 5, 1988.

Digital Library

Google Scholar

Cited By

View all

Iwane HYanami HAnai HKotsireas I(2012)An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for optimization problemsProceedings of the 2011 International Workshop on Symbolic-Numeric Computation10.1145/2331684.2331712(168-177)Online publication date: 7-Jun-2012
https://dl.acm.org/doi/10.1145/2331684.2331712
Iwane HYanami HAnai HYokoyama KSasaki TShirayanagi KKotsireas I(2009)An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier eliminationProceedings of the 2009 conference on Symbolic numeric computation10.1145/1577190.1577203(55-64)Online publication date: 3-Aug-2009
https://dl.acm.org/doi/10.1145/1577190.1577203
Yanami HAnai H(2006)Development of SyNRACProceedings of the 6th international conference on Computational Science - Volume Part II10.1007/11758525_62(462-469)Online publication date: 28-May-2006
https://dl.acm.org/doi/10.1007/11758525_62
Show More Cited By

Index Terms

Quantifier elimination for formulas constrained by quadratic equations

Recommendations

Second Order Quantifier Elimination: Foundations, Computational Aspects and Applications
A formal quantifier elimination for algebraically closed fields
AISC'10/MKM'10/Calculemus'10: Proceedings of the 10th ASIC and 9th MKM international conference, and 17th Calculemus conference on Intelligent computer mathematics

We prove formally that the first order theory of algebraically closed fields enjoys quantifier elimination, and hence is decidable. This proof is organized in two modular parts. We first reify the first order theory of rings and prove that quantifier ...
Negation Elimination from Simple Equational Formulae
ICALP '00: Proceedings of the 27th International Colloquium on Automata, Languages and Programming

Equational formulae are first-order formulae over an alphabet F of function symbols whose only predicate symbol is syntactic equality. Unification problems are an important special case of equational formulae, where no universal quantifiers and no ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ISSAC '93: Proceedings of the 1993 international symposium on Symbolic and algebraic computation

August 1993

321 pages

ISBN:0897916042

DOI:10.1145/164081

Editor:
Manuel Bronstein

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 August 1993

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ISSAC93

Sponsor:

SIGSAM

ISSAC93: International Symposium on Symbolic and Algebraic

July 6 - 8, 1993

Kiev, Ukraine

Acceptance Rates

Overall Acceptance Rate 395 of 838 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
367
Total Downloads

Downloads (Last 12 months)42
Downloads (Last 6 weeks)13

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Iwane HYanami HAnai HKotsireas I(2012)An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for optimization problemsProceedings of the 2011 International Workshop on Symbolic-Numeric Computation10.1145/2331684.2331712(168-177)Online publication date: 7-Jun-2012
https://dl.acm.org/doi/10.1145/2331684.2331712
Iwane HYanami HAnai HYokoyama KSasaki TShirayanagi KKotsireas I(2009)An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier eliminationProceedings of the 2009 conference on Symbolic numeric computation10.1145/1577190.1577203(55-64)Online publication date: 3-Aug-2009
https://dl.acm.org/doi/10.1145/1577190.1577203
Yanami HAnai H(2006)Development of SyNRACProceedings of the 6th international conference on Computational Science - Volume Part II10.1007/11758525_62(462-469)Online publication date: 28-May-2006
https://dl.acm.org/doi/10.1007/11758525_62
Gonzalez-Campos NGonzalez-Vega L(2000)Computing the Cylindrical Algebraic Decomposition Adapted to a Set of EqualitiesComputer Algebra in Scientific Computing10.1007/978-3-642-57201-2_17(203-217)Online publication date: 2000
https://doi.org/10.1007/978-3-642-57201-2_17
Becker ESchmid J(1999)On the Real NullstellensatzAlgorithmic Algebra and Number Theory10.1007/978-3-642-59932-3_9(173-185)Online publication date: 1999
https://doi.org/10.1007/978-3-642-59932-3_9
Dolzmann AGloor OSturm TWeispfenning VTrager B(1998)Approaches to parallel quantifier eliminationProceedings of the 1998 international symposium on Symbolic and algebraic computation10.1145/281508.281564(88-95)Online publication date: 1-Aug-1998
https://dl.acm.org/doi/10.1145/281508.281564
Gemignani LChar BWang P(1997)GCD of polynomials and Bezout matricesProceedings of the 1997 international symposium on Symbolic and algebraic computation10.1145/258726.258808(271-277)Online publication date: 1-Jul-1997
https://dl.acm.org/doi/10.1145/258726.258808
Caprotti O(1993)Extending RISC-CLP(Real) to handle symbolic functionsDesign and Implementation of Symbolic Computation Systems10.1007/BFb0013181(241-255)Online publication date: 1993
https://doi.org/10.1007/BFb0013181

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Second Order Quantifier Elimination: Foundations, Computational Aspects and Applications

A formal quantifier elimination for algebraically closed fields

Negation Elimination from Simple Equational Formulae