On matroids that are transversal and cotransversal

<p>There are distinct differences between classes of matroids that are closed under principal extensions and those that are not Finite-field-representable matroids are not closed under principal extensions and they exhibit attractive properties like well-quasi-ordering and decidable theories (at least for subclasses with bounded branch-width). Infinite-field-representable matroids, on the other hand, are closed under principal extensions and exhibit none of these behaviours. For example, the class of rank-3 real representable matroids is not well-quasi-ordered and has an undecidable theory. The class of matroids that are transversal and cotransversal is not closed under principal extensions or coprincipal coextentions, so we expect it to behave more like the class of finite-field-representable matroids. This thesis is invested in exploring properties in the aforementioned class. A major idea that has inspired the thesis is the investigation of well-quasi-ordered classes in the world of matroids that are transversal and cotransversal. We conjecture that any minor-closed class with bounded branch-width containing matroids that are transversal and cotransversal is well-quasi-ordered. In Chapter 8 of the thesis, we prove this is true for lattice-path matroids, a well-behaved class that falls in this intersection. The general class of lattice-path matroids is not well-quasi-ordered as it contains an infinite antichain of so-called ‘notch matroids’. The interesting phenomenon that we observe is that this is essentially the only antichain in this class, that is, any minor-closed family of lattice-path matroids that contains only finitely many notch matroids is well-quasi-ordered. This answers a question posed by Jim Geelen. Another question that drove the research was recognising fundamental transversal matroids, since these matroids are also cotransversal. We prove that this problem in general is in NP and conjecture that it is NP-complete. We later explore this question for the classes of lattice-path and bicircular matroids. We are successful in finding polynomial-time algorithms in both classes that identify fundamental transversal matroids. We end this part by investigating the intersection of bicircular and cobicircular matroids. We define a specific class - whirly-swirls - and conjecture that eventually any matroid in the above mentioned intersection belongs to this class.</p>

On matroids that are transversal and cotransversal

<p>There are distinct differences between classes of matroids that are closed under principal extensions and those that are not Finite-field-representable matroids are not closed under principal extensions and they exhibit attractive properties like well-quasi-ordering and decidable theories (at least for subclasses with bounded branch-width). Infinite-field-representable matroids, on the other hand, are closed under principal extensions and exhibit none of these behaviours. For example, the class of rank-3 real representable matroids is not well-quasi-ordered and has an undecidable theory. The class of matroids that are transversal and cotransversal is not closed under principal extensions or coprincipal coextentions, so we expect it to behave more like the class of finite-field-representable matroids. This thesis is invested in exploring properties in the aforementioned class. A major idea that has inspired the thesis is the investigation of well-quasi-ordered classes in the world of matroids that are transversal and cotransversal. We conjecture that any minor-closed class with bounded branch-width containing matroids that are transversal and cotransversal is well-quasi-ordered. In Chapter 8 of the thesis, we prove this is true for lattice-path matroids, a well-behaved class that falls in this intersection. The general class of lattice-path matroids is not well-quasi-ordered as it contains an infinite antichain of so-called ‘notch matroids’. The interesting phenomenon that we observe is that this is essentially the only antichain in this class, that is, any minor-closed family of lattice-path matroids that contains only finitely many notch matroids is well-quasi-ordered. This answers a question posed by Jim Geelen. Another question that drove the research was recognising fundamental transversal matroids, since these matroids are also cotransversal. We prove that this problem in general is in NP and conjecture that it is NP-complete. We later explore this question for the classes of lattice-path and bicircular matroids. We are successful in finding polynomial-time algorithms in both classes that identify fundamental transversal matroids. We end this part by investigating the intersection of bicircular and cobicircular matroids. We define a specific class - whirly-swirls - and conjecture that eventually any matroid in the above mentioned intersection belongs to this class.</p>

A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines

We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counterexample guided inductive synthesis principle and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic. Our experiments show that our invariant synthesis framework based on non-provability information can both effectively synthesize inductive invariants and adequately strengthen contracts across a large suite of programs. This work is an extended version of a conference paper titled “Invariant Synthesis for Incomplete Verification Engines”.

First-order and counting theories of ω-automatic structures

The logic extends first-order logic by a generalized form of counting quantifiers (“the number of elements satisfying … belongs to the set C”). This logic is investigated for structures with an injectively ω-automatic presentation. If first-order logic is extended by an infinity-quantifier, the resulting theory of any such structure is known to be decidable [6]. It is shown that, as in the case of automatic structures [21], also modulo-counting quantifiers as well as infinite cardinality quantifiers (“there are many elements satisfying …”) lead to decidable theories. For a structure of bounded degree with injective ω-automatic presentation, the fragment of that contains only effective quantifiers is shown to be decidable and an elementary algorithm for this decision is presented. Both assumptions (ω-automaticity and bounded degree) are necessary for this result to hold.

Degree spectra of prime models

We consider the Turing degrees of prime models of complete decidable theories. In particular we show that every complete decidable atomic theory has a prime model whose elementary diagram is low. We combine the construction used in the proof with other constructions to show that complete decidable atomic theories have low prime models with added properties.If we have a complete decidable atomic theory with all types of the theory computable, we show that for every degree d with 0 < d < 0', there is a prime model with elementary diagram of degree d. Indeed, this is a corollary of the fact that if T is a complete decidable theory and L is a computable set of c.e. partial types of T, then for any degree d > 0, T has a d-decidable model omitting the nonprincipal types listed by L.