Tag Archives: Quasi-automated proofs

Diameter Problem (3)

3. What we will do in this post and and in future posts

We will now try all sorts of ideas to give good upper bounds for the abstract diameter problem that we described. As we explained, such bounds apply to the diameter of graphs of simple d-polytopes.

All the methods I am aware of for providing upper bounds are fairly simple.

(1) You think about a strategy from moving from one set to another, 

(2) You use this strategy to get a recursive bound,

(3) You solve the recursion and hope for the best.

What I would like you to think about, along with reading these posts, is the following questions:

(a) Can I come up with a different/better strategy for moving from one set to the other?

(b) Can I think about a mathematically more sophisticated way to get an upper bound for the diameter?

(c) Can this process of finding a strategy/writing the associated recurrence/solving the recurrence be automatized? The type of proofs we will describe are very simple and this looks like a nice example for a “quasi-automatic” proof process.

Let me repeat the problem and prove to you a nice upper bound:

Reminder: Our Diameter problem for families of sets

Consider a family \cal F of subsets of size d of the set N={1,2,…,n}.

Associate to \cal F a graph G({\cal F}) as follows: The vertices of  G({\cal F}) are simply the sets in \cal F. Two vertices S and T are adjacent if |S \cap T|=d-1.

Continue reading