Cylindrical Decomposition Under Application-Oriented Paradigms

Zylindrische Dekomposition unter anwendungsorientierten Paradigmen

  • Quantifier elimination (QE) is a powerful tool for problem solving. Once a problem is expressed as a formula, such a method converts it to a simpler, quantifier-free equivalent, thus solving the problem. Particularly many problems live in the domain of real numbers, which makes real QE very interesting. Among the so far implemented methods, QE by cylindrical algebraic decomposition (CAD) is the most important complete method. The aim of this thesis is to develop CAD-based algorithms, which can solve more problems in practice and/or provide more interesting information as output. An algorithm that satisfies these standards would concentrate on generic cases and postpone special and degenerated ones to be treated separately or to be abandoned completely. It would give a solution, which is locally correct for a region the user is interested in. It would give answers, which can provide much valuable information in particular for decision problems. It would combine these methods with more specialized ones, for subcases that allow for. ItQuantifier elimination (QE) is a powerful tool for problem solving. Once a problem is expressed as a formula, such a method converts it to a simpler, quantifier-free equivalent, thus solving the problem. Particularly many problems live in the domain of real numbers, which makes real QE very interesting. Among the so far implemented methods, QE by cylindrical algebraic decomposition (CAD) is the most important complete method. The aim of this thesis is to develop CAD-based algorithms, which can solve more problems in practice and/or provide more interesting information as output. An algorithm that satisfies these standards would concentrate on generic cases and postpone special and degenerated ones to be treated separately or to be abandoned completely. It would give a solution, which is locally correct for a region the user is interested in. It would give answers, which can provide much valuable information in particular for decision problems. It would combine these methods with more specialized ones, for subcases that allow for. It would exploit degrees of freedom in the algorithms by deciding to proceed in a way that promises to be efficient. It is the focus of this dissertation to treat these challenges. Algorithms described here are implemented in the computer logic system REDLOG and ship with the computer algebra system REDUCE.show moreshow less

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Andreas Seidl
URN:urn:nbn:de:bvb:739-opus-816
Advisor:Volker Weispfenning
Document Type:Doctoral Thesis
Language:English
Year of Completion:2006
Date of Publication (online):2006/12/06
Publishing Institution:Universität Passau
Granting Institution:Universität Passau, Fakultät für Informatik und Mathematik
Date of final exam:2006/11/30
Release Date:2006/12/06
Tag:CAD; QE; SCAD; cylindrical algebraic decomposition; cylindrical subdecomposition; quantifier elimination
GND Keyword:Quantorenelimination
Institutes:Fakultät für Informatik und Mathematik / Mitarbeiter Lehrstuhl/Einrichtung der Fakultät für Informatik und Mathematik
Dewey Decimal Classification:5 Naturwissenschaften und Mathematik / 51 Mathematik / 510 Mathematik
MSC-Classification:03-XX MATHEMATICAL LOGIC AND FOUNDATIONS / 03Cxx Model theory / 03C10 Quantifier elimination, model completeness and related topics
open_access (DINI-Set):open_access
Licence (German):License LogoStandardbedingung laut Einverständniserklärung