Solving for Sets in Higher-Order Theorem Proving

Chad E. Brown
 

Solving for Sets in Higher-Order Theorem Proving Abstract: Often a key step in a proof is defining a set or relation satisfying desired properties. I will describe new techniques implemented in the TPS higher-order theorem prover which can intertwine searching for proofs with solving for sets.

***********************************************************************
 

Reverse Mathematics and Ergodic Theory

Ksenija Simic

In the book "Subsystems of Second Order Arithmetic" by Stephen Simpson, the author states that the main question of Reverse Mathematics is "Which set existence axioms are needed to prove the theorems of ordinary, non-set-theoretic mathematics?" Here, ordinary means independent of abstract set-theoretic concepts, e.g. all the objects considered are countable or separable. It turns out that in many cases only a few such axioms are repeatedly used. The name "reverse mathematics" comes from the fact that, the reverse is also true - if certain axioms prove a theorem, they are logically equivalent to it. Everything takes place in second order arithmetic. I am going to define the language of second order arithmetic, give axioms for the subsystems that I will be using (RCA0, WKL0, ACA0) and give examples of theorems provable in each. Next I am going to state and explain the Ergodic Theorems in the 'classical' setting and show they can beproved in ACA0, with some modifications. I will explain why the modifications are necessary. Finally, I will briefly talk about applications of Ergodic Theory in other areas of mathematics, in particular number theory, and the research I hope to do in that field.

***********************************************************************

Tournaments in Bounded Arithmetic.

Kerry Emerson Ojakian

An open question posed by Krajicek is whether or not the theory of Bounded Arithmetic can prove "the tournament principle," which states that evey tournament on n vertices has a log n size dominating set. I will present some work we (my advisor and myself) have done on showing that this principle cannot be proved in a weaker subtheory. This is accomplished by using a witnessing theorem, that is a theorem connecting up provability in a theory with a computational procedure of certain complexity. If any of this terminology seems unclear to you, no worry, I'll present some background material so that even someone outside of logic should be able to get it.

***********************************************************************
 

Extending the (1,k)-configuration for Facets of the Knapsack Polytope

David Kravitz

The (1,k)-configuration gives rise to exponentially many facets for certain knapsack inequalities. Here, we generalize this in three different ways, enabling us to easily find exponentially many facets for a much wider range of knapsack inequalities. In addition, the majority of these facets cannot be obtained by sequential lifting of any minimalcover, which can be found easily by other means.

***********************************************************************

b-independent Sets in Random Regular Graphs

Geoffrey Atkinson

A frequenly studied property of graphs is a(G), the largest independent set in G. (A set is independent if it contains no edges). This parameter has been studied in random graphs, G_n,p and G_r, by various authors. In this talk, we will consider a similar concept, a _b(G), the largest b-independent set in a graph G. A set S is said to be b-independent if u,v in S implies d_G(u,v)>b where d _G(u,v) is the shortest distance between u and v in G. We will put the following probabilistic bound on a_b(G_r)$ where G_r is a random regular graph of degree r$on nvertices. Given z> 0, if r \geq r_z, then with probability 1-o(1), 

|a_b(G_r) - 2bn/r^b (log r - b^-1loglog r - b^-1 log{2b}+ b^-1 |<r^-bzn.

***********************************************************************

Equi-integrability in the asymptotic analysis of thin films

Marian Bocea

t is shown that the Dirichlet problem on an arbitrarily large cylinder for fixed affine lateral boundary conditions admits p-equi-integrable minimizing sequences energetically prefering thinner and thinner reference domains. The main ingredient of the proof is a decomposition result for sequences of scaled gradients uniformly bounded in L^p. Joint work with Irene Fonseca.