Below are some applications of HR. Click on the title of the application to read more about that project. Each application is in essence a discovery task, and these have ranged from the inventing of integer sequences through puzzle generation to the prediction of the mutagenic activity of chemicals.
Rules of games from visualisation dataWe have been using HR to learn some rules of a dice game from noisy data supplied from a vision system.
Graph theory ConjecturesWe have been using HR to rediscover some graph theory conjectures that were originally made by the Graffiti program.
Classification Theorems for Finite AlgebrasWe have been using various systems, including Finder, SPASS and HR to generate and prove some classification theorems for finite algebras of particular cardinalities. For instance, Finder generates groups of order 6, and we reduce these to just two isomorphic classes. HR tells us that one difference between the two isomorphism classes is commutativity: groups of size 6 fall into two classes, Abelian and nonAbelian. Then SPASS proves this result. The results for HR working in group, loop, qg4 and qg5quasigroup theory are at the above web page. There's a particularly nice theorem which enables us to classify groups of order 8 by their selfinverse elements.
Zariski SpacesZariski spaces are a new algebraic form, and we are working with Dr. Roy McCasland, an expert in this domain. Our project, funded by a visiting fellowship from EPSRC has two aims:
Although there is still much to do, we have carried out many improvements to HR, and have started looking at the second aim. We are currently running a series of experiments to test the hypothesis that the current version of HR can find something interesting about Zariski spaces. Dr. McCasland has proved that Zariski spaces are semimodules, so, as a first line of attack, we are using HR in semimodule theory to find results which may highlight something interesting about Zariski spaces. Click on the above title to go to the page describing the experiments.
Predicting mutagenecityThe mutagenesis data set is a well known database of chemicals. The chemicals are described in terms of the atoms and bonds between the atoms in the molecules which constitute the chemicals. The task for machine learning programs is to learn a way of predicting whether a particular chemical will be mutagenic (closely related to carcinogenic) or not. Our aim here was to reproduce, and possibly extend the results obtained by the Progol program on a subset of 42 of the chemicals. Finding algebraic discriminantsAs part of a larger tasks, HR was given pairs of algebras and asked to find a discriminant for them, i.e., a property that only one of them had. HR managed to find a discriminant for 97% of the pairs it was presented with. Making conjectures about Maple functionsGiven some functions written for the Maple computer algebra package, we used HR to make conjectures about these functions. We also employed the Otter theorem prover to prove any conjectures it could, so that we could choose to ignore these, as they were likely to follow directly from the definitions of the functions. Comparing and contrasting automated theorem provers
Aiding in tutorial question setting
Inventing puzzles
Generation of implied and induced constraints
Inventing integer sequences
Extrapolating integer sequences
Exploring new algebras

© 2002 Simon Colton 