REDLOG

REDLOG EXAMPLES DOCUMENTATION DOWNLOADS REFERENCES REMIS · REDUCE

References

You are welcome to contact us by email for obtaining copies of our publications.

REDLOG System Papers

These are publications by the REDLOG group. They explicity refer to REDLOG. The content ranges from mathematical foundations to system engineering issues. Publications focussing, in contrast, on the application of REDLOG are collected in the following sections.

  1. Aless Lasaruk and Thomas Sturm. Weak Integer Quantifier Elimination Beyond the Linear Case. In V. G. Ganzha, E. W. Mayr and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing. Proceedings of the CASC 2007: 10th International Workshop, CASC 2007, Bonn, Germany, September 16-20, 2007. Proceedings, volume 4770 of Lecture Notes in Computer Science, pages 275-294, Springer, Berlin, Heidelberg, 2007.
     DOI:10.1007/978-3-540-75187-8_22 -  LOCAL PDF -  REMIS

  2. Thomas Sturm. New Domains for Applied Quantifier Elimination. In Victor G. Ganzha, Ernst W. Mayr and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing: 9th International Workshop, CASC 2006, Chisinau Moldova, September 11-15, 2006, volume 4194 of Lecture Notes in Computer Science, pages 295-301, Springer, Berlin, Heidelberg, 2006.
     DOI:10.1007/11870814_25 -  LOCAL PDF -  REMIS

  3. Christian Straßer. Quantifier Elimination for Queues. In Jan Draisma and Hanspeter Kraft, editors, Rhine Workshop on Computer Algebra. Proceedings of the RWCA 2006, pages 239-248, Universität Basel, Basel, March 2006.
     PUBLIC PDF -  REMIS

  4. Christian Straßer. Quantorenelimination von Queues. Diploma Thesis. Universität Passau, 94030 Passau, Germany, March 2006. In German.
     PUBLIC PDF -  REMIS

  5. Aless Lasaruk and Thomas Sturm. Weak Quantifier Elimination for the Full Linear Theory of the Integers. A Uniform Generalization of Presburger Arithmetic. Technical Report MIP-0604, FMI, Universität Passau, D-94030 Passau, Germany, April 2006. To appear in AAECC.
     www.fmi.uni-passau.de/forschung/mip-beri…richte/MIP-0604.html -  PUBLIC PDF -  REMIS

  6. Christian Hoffelner. Quantifier Elimination-based Parametric Solving in Term Algebras. Diploma Thesis. FMI, Universität Passau, D-94030 Passau, Germany, July 2005.
     PUBLIC PDF -  REMIS

  7. Andreas Dolzmann and Thomas Sturm. Generalized Constraint Solving over Differential Algebras. In V. G. Ganzha, E. W. Mayr and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing. Proceedings of the CASC 2004, pages 111-125, Institut für Informatik, Technische Universität München, 2004.
     wwwmayr.in.tum.de:8080/leabib/advanced.s…lzmann-Sturm%2F04%22 -  LOCAL PDF -  REMIS

  8. Andreas Dolzmann, Andreas Seidl and Thomas Sturm. Efficient Projection Orders for CAD. In Jaime Gutierrez, editor, Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation (ISSAC 2004), pages 111-118, ACM Press, New York, NY, July 2004.
     DOI:10.1145/1005285.1005303 -  LOCAL PDF -  REMIS

  9. Andreas Seidl and Thomas Sturm. Boolean Quantification in a First-Order Context. In V. G. Ganzha, E. W. Mayr and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing. Proceedings of the CASC 2003, pages 329-345, Institut für Informatik, Technische Universität München, 2003.
     wwwmayr.in.tum.de:8080/leabib/advanced.s…2Seidl-Sturm%2F03%22 -  LOCAL PDF -  REMIS

  10. Andreas Seidl and Thomas Sturm. A Generic Projection Operator for Partial Cylindrical Algebraic Decomposition. In Rafael Sendra, editor, Proceedings of the 2003 International Symposium on Symbolic and Algebraic Computation (ISSAC 03) Philadelphia, Pennsylvania, pages 240-247, ACM Press, New York, NY, 2003.
     DOI:10.1145/860854.860903 -  LOCAL PDF -  REMIS

  11. Andreas Dolzmann and Volker Weispfenning. Local Quantifier Elimination. In Carlo Traverso, editor, Proceedings of the 2000 International Symposium on Symbolic and Algebraic Computation (ISSAC 2000) St. Andrews, Scotland, pages 86-94, ACM Press, New York, NY, 2000.
     DOI:10.1145/345542.345589 -  LOCAL PDF -  REMIS

  12. Andreas Dolzmann and Thomas Sturm. P-adic Constraint Solving. In Sam Dooley, editor, Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation (ISSAC 99), Vancouver, BC, pages 151-158, ACM Press, New York, NY, July 1999.
     DOI:10.1145/309831.309894 -  LOCAL PDF -  REMIS

  13. Andreas Dolzmann and Thomas Sturm. Redlog User Manual. Technical Report MIP-9905, FMI, Universität Passau, D-94030 Passau, Germany, April 1999. Edition 2.0 for Version 2.0.
     www.fmi.uni-passau.de/forschung/mip-beri…richte/MIP-9905.html -  PUBLIC PDF -  REMIS

  14. Andreas Dolzmann, Oliver Gloor and Thomas Sturm. Approaches to Parallel Quantifier Elimination. In Oliver Gloor, editor, Proceedings of the 1998 International Symposium on Symbolic and Algebraic Computation (ISSAC 98), Rostock, Germany, pages 88-95, ACM Press, New York, NY, August 1998.
     DOI:10.1145/281508.281564 -  LOCAL PDF -  REMIS

  15. Andreas Dolzmann and Thomas Sturm. Simplification of Quantifier-free Formulae over Ordered Fields. Journal of Symbolic Computation, 24(2):209-231, August 1997.
     DOI:10.1006/jsco.1997.0123 -  LOCAL PDF -  REMIS

  16. Andreas Dolzmann and Thomas Sturm. Redlog: Computer Algebra Meets Computer Logic. ACM SIGSAM Bulletin, 31(2):2-9, June 1997.
     DOI:10.1145/261320.261324 -  LOCAL PDF -  REMIS

  17. Thomas Sturm. Lineare Quantorenelimination in bewerteten Körpern. D-94030 Passau, Germany, February 1995.
     REMIS

REDLOG Applications

These are publications by the REDLOG group on applications of REDLOG to problems from various areas. Publications on the application of REDLOG by others are collected in the following section.
  1. Thomas Sturm. Quantifier Elimination for Constraint Logic Programming. In Victor G. Ganzha, Ernst W. Mayr and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing: 8th International Workshop, CASC 2005, Kalamata, Greece September 12-16, 2005, volume 3718 of Lecture Notes in Computer Science, pages 416-430, Springer, Berlin, Heidelberg, 2005.
     DOI:10.1007/11555964_36 -  REMIS

  2. Thomas Sturm. Integration of quantifier elimination with constraint logic programming. In Jacques Calmet et al., editor, Artificial Intelligence, Automated Reasoning, and Symbolic Computation. Joint International Conference, AISC 2002 and Calculemus 2002 Marseille France, July 1-5, 2002 Proceedings, volume 2385 of Lecture Notes in Artificial Intelligence (Subseries of LNCS), pages 7-11, Springer-Verlag, Berlin, Heideberg, 2002.
     www.springerlink.com/content/vvh5t7tpfbg8ykph/ -  REMIS

  3. Volker Weispfenning. Semilinear Motion Planning in REDLOG. Applicable Algebra in Engineering, Communication and Computing, 12:455-475, June 2001.
     DOI:10.1007/s002000100086 -  REMIS

  4. Andreas Dolzmann and Thomas Sturm. Parametric Systems of Linear Congruences. In V. G. Ganzha, E. W. Mayr and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing. Proceedings of the CASC 2001, pages 149-166, Springer, Berlin, 2001.
     www.amazon.com/Computer-Algebra-Scientif…7559?ie=UTF8&s=books -  REMIS

  5. Hirokazu Anai and Volker Weispfenning. Reach set computations using real quantifier elimination. In Hybrid Systems, Computation and Control (HSCC 2001), volume 2034 of Lecture Notes in Computer Science, Springer, 2001.
     www.springerlink.com/content/14g2k8gyjwqy65j8/ -  REMIS

  6. Thomas Sturm. An algebraic approach to offsetting and blending of solids. In V. G. Ganzha, E. W. Mayr and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing. Proceedings of the CASC 2000, pages 367-382, Springer, Berlin, 2000.
     www.amazon.com/Computer-Algebra-Scientif…7559?ie=UTF8&s=books -  REMIS

  7. Thomas Sturm. Real Quantifier Elimination in Geometry. Doctoral Dissertation. Department of Mathematics and Computer Science. University of Passau, Germany, D-94030 Passau, Germany, December 1999.
     PUBLIC PDF -  REMIS

  8. Thomas Sturm. Reasoning over Networks by Symbolic Methods. Applicable Algebra in Engineering Communication and Computing, 10(1):79-96, September 1999.
     DOI:10.1007/s002000050123 -  LOCAL PDF -  REMIS

  9. Andreas Dolzmann. Solving Geometric Problems with Real Quantifier Elimination. Technical Report MIP-9903, FMI, Universität Passau, D-94030 Passau, Germany, January 1999.
     www.fmi.uni-passau.de/forschung/mip-beri…richte/MIP-9903.html -  PUBLIC PDF -  REMIS

  10. Thomas Sturm and Volker Weispfenning. Computational Geometry Problems in Redlog. In Dongming Wang, editor, Automated Deduction in Geometry, volume 1360 of Lecture Notes in Artificial Intelligence (Subseries of LNCS), pages 58-86, Springer-Verlag, Berlin Heidelberg, 1998.
     DOI:10.1007/BFb0022720 -  LOCAL PDF -  REMIS

  11. Andreas Dolzmann. Solving Scheduling Problems with REDLOG. Extended abstract at the Rhine Workshop on Computer Algebra, April 1998.
     REMIS

  12. Andreas Dolzmann, Thomas Sturm and Volker Weispfenning. Real Quantifier Elimination in Practice. In B. H. Matzat, G.-M. Greuel and G. Hiss, editors, Algorithmic Algebra and Number Theory, pages 221-247, Springer, Berlin, 1998.
     www.amazon.com/Algorithmic-Algebra-Numbe…7559?ie=UTF8&s=books -  REMIS

  13. Andreas Dolzmann, Thomas Sturm and Volker Weispfenning. A New Approach for Automatic Theorem Proving in Real Geometry. Journal of Automated Reasoning, 21(3):357-380, 1998.
     DOI:10.1023/A:1006031329384 -  REMIS

  14. Volker Weispfenning. Simulation and Optimization by Quantifier Elimination. Journal of Symbolic Computation, 24(2):189-208, August 1997. Special issue on applications of quantifier elimination.
     DOI:10.1006/jsco.1997.0122 -  LOCAL PDF -  REMIS

  15. Thomas Sturm and Volker Weispfenning. Rounding and Blending of Solids by a Real Elimination Method. In Achim Sydow, editor, Proceedings of the 15th IMACS World Congress on Scientific Computation, Modelling, and Applied Mathematics (IMACS 97), volume 2 , pages 727-732, Wissenschaft & Technik Verlag, Berlin, August 1997.
     sab.sscc.ru/Imacs_97 -  REMIS

  16. Andreas Dolzmann and Thomas Sturm. Guarded Expressions in Practice. In Wolfgang W. Küchlin, editor, Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation (ISSAC 97), Maui, HI, pages 376-383, ACM Press, New York, NY, July 1997.
     DOI:10.1145/258726.258851 -  REMIS

REDLOG Third-Party Applications

These are publications by external people on applications of REDLOG to problems from various areas. Any information on further such publications not yet listed here is highly appreciated.
  1. Viorica Sofronie-Stokkermans. Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions. In B. Konev and F. Wolter, editors, Frontiers of Combining Systems. 6th International Symposium, FroCoS 2007 Liverpool, UK, September 10-12, 2007 Proceedings, volume 4720 of LNAI, pages 47-71, Springer, Berlin Heidelberg, Germany, 2007.
     DOI:10.1007/978-3-540-74621-8_3 -  LOCAL PDF -  REMIS

  2. Christopher W. Brown, M'hammed El Kahoui, Dominik Novotni and Andreas Weber. Algorithmic methods for investigating equilibria in epidemic modeling. Journal of Symbolic Computation, 41(11):1157-1173, November 2006. Special Issue on the Occasion of Volker Weispfenning's 60th Birthday.
     DOI:10.1016/j.jsc.2005.09.011 -  LOCAL PDF -  REMIS

  3. Hugh Anderson, Siau-Cheng Khoo, Stefan Andrei and Beatrice Luca. Calculating Polynomial Runtime Properties. In K. Yi, editor, Programming Languages and Systems. Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005. Proceedings, volume 3780 of LNCS, pages 230-245, Springer, Berlin Heidelberg, Germany, 2005.
     DOI:10.1007/11575467_16 -  LOCAL PDF -  REMIS

  4. Werner M. Seiler and Andreas Weber. Deciding Ellipticity by Quantifier Elimination. In V. G. Ganzha, E. W. Mayr and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing. Proceedings of the CASC 2003, pages 347-355, Institut für Informatik, Technische Universität München, 2003.
     wwwmayr.in.tum.de:8080/leabib/advanced.s…Seiler-Weber%2F03%22 -  REMIS

  5. M'hammed Kahoui and Andreas Weber. Symbolic Equilibrium Point Analysis in Parameterized Polynomial Vector Fields. In Victor G. Ganzha, Ernst W. Mayr and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing. Proceedings of the CASC 2002, pages 71-83, Institut für Informatik, Technische Universität München, 2002.
     wwwmayr.in.tum.de/konferenzen/CASC2002/C…002/CD/casc02-8.html -  LOCAL PDF -  REMIS

  6. Gerardo Lafferriere, George J. Pappas and Sergio Yovine. Symbolic Reachability Computation for Families of Linear Vector Fields. Journal of Symbolic Computation, 32(3):231-253, 2001.
     DOI:10.1006/jsco.2001.0472 -  LOCAL PDF -  REMIS

  7. Nikolaos I. Ioakimidis. Finite Differences/Elements in Classical Beam Problems: Derivation of Feasibility Conditions Under Parametric Inequality Constraints with the Help of Reduce and REDLOG. Computational Mechanics, 27(2):145-153, February 2001.
     DOI:10.1007/s004660000223 -  LOCAL PDF -  REMIS

  8. M'hammed Kahoui and Andreas Weber. Deciding Hopf Bifurcations by Quantifier Elimination in a Software Component Architecture. Journal of Symbolic Computation, 30(2):161-179, August 2000.
     DOI:10.1006/jsco.1999.0353 -  LOCAL PDF -  REMIS

  9. Nikolaos I. Ioakimidis. Automatic Derivation of Positivity Conditions Inside Boundary Elements with the Help of the REDLOG Computer Logic Package. Engineering Analysis with Boundary Elements, 23(10):847-856, December 1999.
     DOI:10.1016/S0955-7997(99)00049-1 -  LOCAL PDF -  REMIS

  10. Nikolaos I. Ioakimidis. REDLOG-Aided Derivation of Feasibility Conditions in Applied Mechanics and Engineering Problems Under Simple Inequality Constraints. Journal of Mechanical Engineering (Strojnicky Casopis), 50(1):58-69, 1999.
     www.strojcas.sav.sk/sc1-99.htm -  LOCAL PDF -  REMIS

Theoretical Foundations of REDLOG

These are theoretical papers not explicitly referring to REDLOG. Algorithms described therin are used within REDLOG. Theoretical papers explicitly referring to REDLOG are generally listed as REDLOG System Papers above.
  1. Thomas Sturm and Volker Weispfenning. Quantifier Elimination in Term Algebras. The Case of Finite Languages. In Victor G. Ganzha, Ernst W. Mayr and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing. Proceedings of the CASC 2002, pages 285-300, Institut für Informatik, Technische Universität München, 2002.
     wwwmayr.in.tum.de/konferenzen/CASC2002/C…02/CD/casc02-30.html -  REMIS

  2. Thomas Sturm. Linear Problems in Valued Fields. Journal of Symbolic Computation, 30(2):207-219, August 2000.
     DOI:10.1006/jsco.1999.0303 -  LOCAL PDF -  REMIS

  3. Volker Weispfenning. Quantifier elimination for real algebra---the quadratic case and beyond. Applicable Algebra in Engineering Communication and Computing, 8(2):85-101, February 1997.
     DOI:10.1007/s002000050055 -  LOCAL PDF -  REMIS

  4. Volker Weispfenning. Parametric Linear and Quadratic Optimization by Elimination. Technical Report MIP-9404, FMI, Universität Passau, D-94030 Passau, Germany, April 1994.
     www.fmi.uni-passau.de/forschung/mip-beri…richte/MIP-9404.html -  PUBLIC PDF -  REMIS

  5. Rüdiger Loos and Volker Weispfenning. Applying Linear Quantifier Elimination. The Computer Journal, 36(5):450-461, 1993. Special issue on computational quantifier elimination.
     DOI:10.1093/comjnl/36.5.450 -  LOCAL PDF -  REMIS

  6. George E. Collins and Hoon Hong. Partial Cylindrical Algebraic Decomposition for Quantifier Elimination. Journal of Symbolic Computation, 12(3):299-328, September 1991.
     REMIS

  7. Volker Weispfenning. The Complexity of Linear Problems in Fields. Journal of Symbolic Computation, 5(1-2):3-27, February-April 1988.
     LOCAL PDF -  REMIS

A.D. T.S. www@redlog.eu Validate