New Domains for Applied Quantifier Elimination

13 years 11 months ago
New Domains for Applied Quantifier Elimination
We address various aspects of our computer algebra-based computer logic system redlog. There are numerous examples in the literature for successful applications of redlog to practical problems. This includes work by the group around the redlog developers as well as by many others. redlog is, however, not at all restricted to the real numbers but comprises a variety of other domains. We particularly point at the immense potential of quantifier elimination techniques for the integers. We also address another new redlog domain, which is queues over arbitrary basic domains. Both have most promising applications in practical computer science, viz. automatic loop parallelization and software security. 1 REDLOG The redlog package of the computer algebra system reduce extends the idea of symbolic computation from computer algebra to first-order logic [1, 2, 3, 4]. It provides an integrated interactive environment for computing with first-oder formulas over temporarily fixed languages and domai...
Thomas Sturm
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CASC
Authors Thomas Sturm
Comments (0)