Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 20 of 20 for “"quantifier elimination"”.
-
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 …
-
Quantifier elimination and decidability of the theory of additive integer group augmented by predicates of multiplicative cyclic submonoids
Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-11-14 without embargo terms
-
Verification of advanced controllers for safety-critical systems
… as the Satisfiability Modulo Theories (SMT) and quantifier elimination (Weispfenning’s virtual term substitution and quantifier elimination by cylindrical algebraic decomposition) algorithms. Any control design requirement (such as satisfactory performance, robustness to uncertainties, stability, …
-
Model theory and probability
… logic. The author studies axioms, type spaces, quantifier elimination, separable categoricity, saturated models, stability, and d-finiteness for the theories of atomless probability algebras and atomless random variable structures. Explicit formulas for the d*-metric between types in the theory …
-
Modest Automorphisms of Presburger Arithmetic
… that enable us in Chapters 4 and 5 to prove quantifier elimination, decidability, and axiomatizability for both the quotient and the Presburger structure expanded by this automorphism, with explicit axiomatizations given in Chapter 3. The second automorphism is maximal in the sense that its …
-
Model Theory of Nakano Spaces
… fixed compact essential range is shown to admit quantifier elimination. It is also shown that if this essential range is moreover bounded away from 1, the latter theory is model-theoretically stable.
-
Model theory of algebraically closed fields and the Ax-Grothendieck Theorem
… results about algebraically closed fields is the quantifier elimination property. We also show that the theory of algebraically closed field with a given characteristic is complete and model-complete. Finally, we introduce the beautiful Ax-Grothendieck theorem and an application to it.
-
Differential dynamic logics - automated theorem proving for hybrid systems
… free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid systems successively to properties of their parts. Our main result proves that this calculus axiomatises the transition …
-
Model Theory of Real -Trees and Their Isometries
… companion of the theory of real-trees that has quantifier elimination, is complete and is stable but not superstable. The model theoretic independence relation for the model companion is described and it is shown that it is not categorical in any infinite cardinal. Next it is shown that various …
-
Upper and Lower Complexity Bounds for Some Problems in Elementary Geometry
… is used to encode polynomials, the length of any quantifier-free formula expressing the set I (2n,n) is bounded from below by Ω(c n ). Other related complexity results are stated; in particular, a lower bound for algebraic computation trees based on the notion of limiting hypersurface is …
-
On asymptotic valued differential fields with small derivation
… (such pre-$H$-fields necessarily have gap 0) has quantifier elimination in the language $\{+, -, \cdot, 0, 1, \leqslant, \preccurlyeq, \der\}$. From quantifier elimination, we deduce that this theory is complete and is the model completion of the theory of pre-$H$-fields with gap 0 (equivalently, …
-
Cylindrical Decomposition Under Application-Oriented Paradigms
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 …
-
Logical representations for automated reasoning about spatial relationships
… are dealt with: a decision procedure based on quantifier elimination is given for a large class of formulae within a 1st-order topological language; reasoning mechanisms based on the composition of spatial relations are studied; the non-topological property of convexity is examined both from …
-
The computational complexity of prefix classes of logical theories
… $<$, +, 2$\sp{x}\rangle$ by analyzing the quantifier elimination procedure for this theory described by Gottsch. We show that the formulas in $\Sigma\sb{m}\cup\Pi\sb{m}$ in this theory can be decided in $NSPACE$(exp$\sb{m}(cmn\sp3))$. Finally we get close upper and lower bounds for the …
-
Formal verification of analog and mixed signal circuits using deductive and bounded approaches
… Formulas (FOFs) having Universal-Existential quantifiers. A tractable numeric-symbolic approach, based on SOS programming and Quantifier Elimination (QE), is used to verify these FOFs. The approach is applied to the verification of inevitability of oscillation in ROs with odd and even …
-
The Challenges of Non-linear Parameters and Variables in Automatic Loop Parallelisation
… such schedules can be expressed easily as a quantifier elimination problem but this approach turns out to be computationally less efficient with the available implementation. As a second transformation, we study parametric tiling which is used to adapt a parallelised program to the number of …
-
Automata-based decision procedures for weak arithmetics
… with the <br>automata for formulas produced by a quantifier elimination method. We <br>also show that this triple exponential bound is tight. Moreover, we <br>provide optimal automata constructions for linear equations and <br>inequations, and present new techniques for mechanizing an …
-
Abstractions for Reverse Engineering
Increasingly sophisticated systems are being integrated into our daily lives, raising the need to verify their safety and reliability. Formal methods offer a range of techniques for providing sound guarantees of a system's correctness with respect to its specification. The continuous evolution of …
-
Symbolic Approaches for Boolean Synthesis
Boolean synthesis is the problem defined as the procedure to construct solutions for unknown variables in a given specification in Boolean formula as a conjunction of constraints describing the relationship over known and unknown variables. Formally, the problem consists of two parts, the …
-
Algebraically closed fields with characters; differential-henselian monotone valued differential fields
This thesis consists of two unrelated research projects. In the first project we study the model theory of the 2-sorted structure (F, C; χ), where F is an algebraic closure of a finite field of characteristic p, C is the field of complex numbers and χ ∶ F → C is an injective, multiplication …