Craig Larson, Department of Mathematics and Applied Mathematics, Virginia Commonwealth UniversityDepartment
Automated Conjecturing for Proof Discovery
CONJECTURING is an open-source Sage program which can be used to make
invariant-relation or property-relation conjectures for any mathematical object-type.
The user must provide at least a few object examples, together with functions
defining invariants and properties for that object-type. These invariants and
properties will then appear in the conjectures.
Here we demonstrate how the CONJECTURING program can be used to produce proof
sketches in graph theory. In particular, we are interested in graphs where the
independence number of the graph equals its residue. Residue is a very good lower
bound for the independence number - and the question of characterizing the class of
graphs where these invariants are equal has been of continuing interest. The
CONJECTURING program can be used to generate both necessary and sufficient condition
conjectures for graphs where the independence number equals its residue, and proof
sketches of these conjectures can also be generated.
We will discuss the program and give examples. This is joint work with Nico Van
Cleemput (Ghent University).