2 1. INTRODUCTION

Other authors who have studied families of binary matroids with no minors

in some subset of {F7, F7 ∗, M(K3,3), M(K5), M ∗(K3,3), M ∗(K5)} include Wal-

ton and Welsh [WW80], who examine the characteristic polynomials of ma-

troids in such classes, and Kung [Kun86], who has considered the maximum

size obtained by a simple rank-r matroid in one of these classes. Qin and

Zhou [QZ04] have characterized the internally 4-connected binary matroids with

no minor in {M(K3,3), M(K5), M ∗(K3,3), M ∗(K5)}. Moreover Zhou [Zho08]

has also characterized the internally 4-connected binary matroids that have no

M(K3,3)-minor, but which do have an M(K5)-minor. Finally we note that the

classic result of Hall [Hal43] on graphs with no K3,3-minor leads to a char-

acterization of the internally 4-connected binary matroids with no minor in

{F7, F7

∗,

M

∗(K3,3),

M

∗(K5),

M(K3,3)}, and Wagner’s [Wag37] theorem on the

graphs with no K5-minor leads to a characterization of the internally 4-connected

binary matroids with no minor in {F7, F7

∗,

M

∗(K3,3),

M

∗(K5),

M(K5)}.

The proof of Theorem 1.1 is unusual amongst results in matroid theory, in that

we rely upon a computer to check certain facts. All these checks have been carried

out using the software package Macek, developed by Petr Hlinˇ en´ y. In addition we

have written software, which does not depend upon Macek, to provide us with an

independent check of the same facts.

The Macek package is available to download, along with supporting documen-

tation. The current website is http://www.fi.muni.cz/~hlineny/MACEK. Thus

the interested reader is able to download Macek and confirm that it verifies our

assertions. Points in the proof where a computer check is required are marked by

a marginal symbol and a number. The numbers provide a reference for the web-

site of the second author (current url: http://www.maths.uwa.edu.au/~gordon),

which contains a more detailed description of the steps taken to verify each asser-

tion, and the intermediate data produced during that computer check.

We emphasize that none of the computer tests relies upon an exhaustive search

of all the matroids of a particular size or rank. The only tasks a program need

perform to verify our checks are: determine whether two binary matroids are iso-

morphic; check whether a binary matroid has a particular minor; and, generate all

the single-element extensions and coextensions of a binary matroid. Whenever the

proof requires a computer check, the text includes a complete description (inde-

pendent of any particular piece of software) of the tasks that we ask the computer

to perform. Hence a reader who is able to construct software with the capabilities

listed above could provide another verification of our assertions.

The article is organized as follows: In Chapter 2 we develop the basic definitions

and results we will need to prove Theorem 1.1. In Chapter 3 we introduce the

M¨ obius matroids and consider their properties in detail.

Chapter 4 is concerned with showing that a minimal counterexample to Theo-

rem 1.1 can be assumed to be vertically 4-connected. This chapter depends heavily

upon the Δ-Y operation and its dual; we make extensive use of results proved

by Oxley, Semple, and Vertigan [OSV00]. The central idea of Chapter 4 is that

if a binary matroid M with no M(K3,3)-minor is non-cographic and internally

4-connected but not vertically 4-connected, then by repeatedly performing Y -Δ

operations, we can produce a vertically 4-connected non-cographic binary matroid