HR home Theory of theory formation Applications of HR HR manual Projects using HR Download HR

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 data

We have been using HR to learn some rules of a dice game from noisy data supplied from a vision system.

Graph theory Conjectures

We have been using HR to re-discover some graph theory conjectures that were originally made by the Graffiti program.

Classification Theorems for Finite Algebras

We 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 non-Abelian. Then SPASS proves this result. The results for HR working in group, loop, qg4 and qg5-quasigroup theory are at the above web page. There's a particularly nice theorem which enables us to classify groups of order 8 by their self-inverse elements.

Zariski Spaces

Zariski 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:

  • To take HR a step closer towards being used by research mathematicians. Dr. McCasland's input to this has been to use and criticise HR, and Dr. Colton has carried out some of the improvements to the functionality of HR suggested by Dr. McCasland.
  • To use the improved version of HR to find interesting results about Zariski spaces.

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 mutagenecity

The 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 discriminants

As 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 functions

Given 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