Quantifier Elimination over Real Closed Fields- Mathematical Basis Solution Techniques Practical Integrations

This work investigates the quantifier elimination problem in real closed fieldswith respect to the application in description logics. The motivation for theinvestigation in this topic is mainly based on the demand for an extension ofdescription logic systems to support a default concrete domain for non-linearmultivariate equations and inequations. The authors provide a literatureoverview that summarizes main mathematical tools for checking whether aset of non-linear multivariate (in-)equatins is satisfiable (quantifier eliminationproblem). The authors shortly describe how application examples are handledwith a prototype implementation.