Algorithmic strategies for applicable real quantifier elimination

One of the most important algorithms for real quantifier elimination is the quantifier elimination by virtual substitution introduced by Weispfenning in 1988. In this thesis we present numerous algorithmic approaches for optimizing this quantifier elimination algorithm. Optimization goals are the actual running time of the implementation of the algorithm and the size of the output formula. Strategies for obtaining these goals include simplification of first-order formulas,reduction of the size of the computed elimination set, and condensing a new replacement for the virtual substitution. Local quantifier elimination computes formulas that are equivalent to the input formula only nearby a given point. We can make use of this restriction for further optimizing the quantifier elimination by virtual substitution. Finally we discuss how to solve a large class of scheduling problems by real quantifier elimination. To optimize our algorithm for solving scheduling problems we make use of the special form of the input formula and of additional information given by the description of the scheduling problem

Level thesis:degree_level

thesis.doctoral

Grantor dc:publisher

Universität Passau

Year

2000

Author dc:creator

• Dolzmann, Andreas

Contributors dc:contributor

• Weispfenning, Volker

• Scheduling
• Formeln erster Stufe
• Quantifier elimination
• simplification
• first-order formulas

Statement dc:rights

• Standardbedingung laut Einverständniserklärung

Repository record source_url

https://opus4.kobv.de/opus4-uni-passau/frontdoor/index/index/docId/4

OAI identifier oai:identifier

oai:kobv.de-opus4-uni-passau:4