REDLOG

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

REDLOG: computer algebra meets computer logic

Full text

Pdf (802 KB)

Source

ACM SIGSAM Bulletin archive
Volume 31 , Issue 2 (June 1997) table of contents

Pages: 2 - 9

Year of Publication: 1997

ISSN:0163-5824

Authors

Andreas Dolzmann	Department of Mathematics and Computer Science, University of Passau, Germany
Thomas Sturm	Department of Mathematics and Computer Science, University of Passau, Germany

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 15, Citation Count: 25

Additional Information:

abstract cited by index terms collaborative colleagues

Tools and Actions:	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/261320.261324 What is a DOI?

ABSTRACT

REDLOG is a package that extends the computer algebra system REDUCE to a computer logic system, i.e., a system that provides algorithms for the symbolic manipulation of first-order formulas over some temporarily fixed language and theory. In contrast to theorem provers, the methods applied know about the underlying algebraic theory and make use of it. We illustrate some applications of REDLOG, describe its functionality as it appears to the user, and explain the design issues and implementation techniques. REDLOG is available on the WWW.

CITED BY 25

	Andreas Dolzmann , Oliver Gloor , Thomas Sturm, Approaches to parallel quantifier elimination, Proceedings of the 1998 international symposium on Symbolic and algebraic computation, p.88-95, August 13-15, 1998, Rostock, Germany
	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
	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
	Andreas Dolzmann , Volker Weispfenning, Local quantifier elimination, Proceedings of the 2000 international symposium on Symbolic and algebraic computation, p.86-94, July 2000, St. Andrews, Scotland
	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
	Christopher W. Brown, QEPCAD B: a program for computing with semi-algebraic sets using CADs, ACM SIGSAM Bulletin, v.37 n.4, December 2003
	Gerardo Lafferriere , George J. Pappas , Sergio Yovine, Symbolic Reachability Computation for Families of Linear Vector Fields, Journal of Symbolic Computation, v.32 n.3, p.231-253, 09/01/2001
	Torsten Robschink , Gregor Snelting, Efficient path conditions in dependence graphs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Andreas Dolzmann , Andreas Seidl , Thomas Sturm, Efficient projection orders for CAD, Proceedings of the 2004 international symposium on Symbolic and algebraic computation, p.111-118, July 04-07, 2004, Santander, Spain
	Sriram Sankaranarayanan , Henny B. Sipma , Zohar Manna, Non-linear loop invariant generation using Gröbner bases, ACM SIGPLAN Notices, v.39 n.1, p.318-329, January 2004
	Andreas Seidl , Thomas Sturm, A generic projection operator for partial cylindrical algebraic decomposition, Proceedings of the 2003 international symposium on Symbolic and algebraic computation, p.240-247, August 03-06, 2003, Philadelphia, PA, USA
	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
	Andreas Dolzmann , Volker Weispfenning, Multiple object semilinear motion planning, Journal of Symbolic Computation, v.42 n.3, p.324-337, March, 2007
	Akira Suzuki , Yosuke Sato, A simple algorithm to compute comprehensive Gröbner bases using Gröbner bases, Proceedings of the 2006 international symposium on Symbolic and algebraic computation, July 09-12, 2006, Genoa, Italy
	Akira Suzuki , Yosuke Sato, Implementation of CGS and CGB on Risa/Asir and other computer algebra systems using Suzuki-Sato algorithm, ACM Communications in Computer Algebra, v.41 n.3, September 2007 issue 161
	Swen Jacobs , Viorica Sofronie-Stokkermans, Applications of Hierarchical Reasoning in the Verification of Complex Systems, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.8, p.39-54, June, 2007
	Assia Mahboubi, Implementing the cylindrical algebraic decomposition within the Coq system, Mathematical Structures in Computer Science, v.17 n.1, p.99-127, February 2007
	Katsusuke Nabeshima, PGB: a package for computing parametric Gröbner and related objects, ACM Communications in Computer Algebra, v.41 n.3, September 2007 issue 161
	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
	Katsusuke Nabeshima, A speed-up of the algorithm for computing comprehensive Gröbner systems, Proceedings of the 2007 international symposium on Symbolic and algebraic computation, July 29-August 01, 2007, Waterloo, Ontario, Canada
	Christopher W. Brown , James H. Davenport, The complexity of quantifier elimination and cylindrical algebraic decomposition, Proceedings of the 2007 international symposium on Symbolic and algebraic computation, July 29-August 01, 2007, Waterloo, Ontario, Canada
	Bican Xia, DISCOVERER: a tool for solving semi-algebraic systems, ACM Communications in Computer Algebra, v.41 n.3, September 2007 issue 161
	Dario Campagna , Carla Piazza, Hybrid Automata in Systems Biology: How Far Can We Go?, Electronic Notes in Theoretical Computer Science (ENTCS), v.229 n.1, p.93-108, February, 2009
	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