New concepts for real quantifier elimination by virtual substitution
Marek Košta · Max Planck Digital Library · 2016
Quantifier elimination methods for real closed fields are an intensively studied subject from both theoretical and practical points of view. This thesis studies quantifier elimination based on virtual substitution with a particular focus on practically applicable methods and techniques. We develop a novel, stand-alone, and modular quantifier elimination framework for virtual substitution that can in principle be extended to arbitrary but bounded degrees of quantified variables. The framework subsumes previous virtual substitution algorithms. Quantifier elimination algorithms are obtained via instantiation of our quantifier elimination algorithm scheme with three precisely specified subalgorithms. We give instantiations of our scheme up to degree three of a quantified variable, which yields a quantifier elimination algorithm by virtual substitution for the cubic case. Compared to previous virtual substitution-based approaches, we propose novel improvements like smaller elimination sets and clustering. Furthermore, we exploit the Boolean structure and develop a structural quantifier elimination algorithm scheme. This allows us to take advantage of subformulas containing equations or negated equations, simplify virtual substitution results, and develop flexible bound selection strategies. We also revisit the established technique of degree shifts and show how to generalize this within our structural quantifier elimination algorithm scheme. Restricting ourselves to existential problems, we address the established concept of extended quantified elimination, which in addition to quantifier-free equivalents yields answers for existentially quantified variables. We show how to realize this concept within our quantifier elimination algorithm scheme. Moreover, we generalize our post-processing method for eliminating nonstandard symbols from answers to the general case. Our implementation of most of the concepts developed in this thesis is the first implementation of a cubic virtual substitution method. Experimental results comparing our implementation with the established original implementation of the quadratic virtual substitution in the Redlog computer logic system demonstrate the relevance of our novel techniques: On more than two hundred quantifier elimination problems---considered in more than sixty scientific publications during the past twenty years---we never eliminate fewer quantifiers than the Redlog's original implementation. For a considerable number of problems we eliminate more quantifiers. Quantoreneliminationsverfahren fur reelle abgeschlossene Korper sind sowohl von der theoretischen als auch von der praktischen Seite ein intensiv studiertes Thema. Diese Dissertation befasst sich mit Quantorenelimination basierend auf virtueller Substitution. Im Mittelpunkt stehen praktisch anwendbare Methoden und Techniken. Wir entwicklen ein neues, unabhangiges und modulares Quantoreneliminationsrahmenkonzept fur virtuelle Substitution, das im Prinzip auf beliebige Grade von quantifizierten Variablen erweitert werden kann. Unser Rahmenkonzept subsumiert existierende auf virtueller Substitution beruhende Algorithmen. Konkrete Algorithmen enstehen als Instanzen unseres Quantoreneliminationsalgorithmusschemas mit drei genau spezifizierten Subalgorithmen. Wir prasentieren Instanzen bis zu Grad drei einer quantifizierten Variable. Die liefern einen Algorithmus beruhend auf virtueller Substitution fur den kubischen Fall. Im Vergleich mit anderen Verfahren basierend auf virtueller Substitution prasentieren wir zahlreiche Verbesserungen wie etwa kleinere Eliminationsmengen oder Clustering. Auserdem nutzen wir die Boolsche Struktur aus und entwickeln ein strukturelles Quantoreneliminationsalgorithmusschema. Somit konnen wir Gleichungen oder negierte Gleichungen ausnutzen, Ergebnisse der virtuellen Substitution vereinfachen und flexible Schrankenauswahlstrategien entwickeln. Wir studieren auch die bekannte Technik des degree shifts, die in manchen Fallen den Grad der quantifizierten Variablen reduzieren kann. Wir zeigen wie man diese Technik in unserem Quantoreneliminationsalgorithmusschema realisiert und verallgemeinert. Fur reelle existentielle Probleme diskutieren wir das Konzept der erweiterten Quantorenelimination, die zu quantorenfreien Aquivalenten auch Antworten fur die quantifizierten Variablen liefert. Wir zeigen wie sich dieses Konzept in unserem Quantoreneliminationsalgorithmusschema realisieren lasst. Zusatzlich verallgemeinern wir unser Postprocessingverfahren zur Elimination von Nichtstandardsymbolen aus Antworten. Unsere Implementierung unterstutzt die meisten in dieser Arbeit vorgestellte Konzepte und stellt damit die erste Implementierung einer kubischen Methode basierend auf virtueller Substitution dar. Praktische Rechenexperimente, in denen wir unsere Implementierung mit bekannten im Computerlogik-System Redlog implementierten Verfahren fur quadratische virtuelle Substitution verglichen, zeigen die Relevanz unserer Techniken: Auf mehr als 200 in mehr als sechzig wissenschaftlichen Publikationen beschriebenen Quantoreneliminationsproblemen eliminiert unsere Implementierung niemals weniger Quantoren als die existierende Implementierung in Redlog. Fur eine signifikante Anzahl von Problemen konnen wir sogar mehr Quantoren eliminieren.