ILP for Mathematical Discovery

We believe that AI programs written for discovery tasks will need to simultaneously employ a variety of reasoning techniques such as induction, abduction, deduction, calculation and invention. We describe the HR system which performs a novel ILP routine called automated theory formation. This combines inductive and deductive reasoning to form clausal theories consisting of classification rules and association rules. HR generates definitions using a set of production rules, interprets the definitions as classification rules, then uses the success sets of the definitions to induce hypotheses from which it extracts association rules. It uses third party theorem provers and model generators to check whether the association rules are entailed by a set of user supplied axioms. HR has been applied to a range of predictive, descriptive and subgroup discovery tasks in domains of pure mathematics. We describe these applications and how they have led to some interesting mathematical discover...

• Type: Conference
• Year: 2003
• Where: ILP
• Authors: Simon Colton, Stephen Muggleton
• Keywords: Association Rules, Classification Rules, Discovery Tasks, ILP 2003