Automatic construction and verification of isotopy invariants

Volker Sorge, Andreas Meier, Roy McCasland, Simon Colton

Research output: Contribution to journalArticleResearchpeer-review

9 Citations (Scopus)

Abstract

We extend our previous study of the automatic construction of isomorphicclassification theorems for algebraic domains by considering the isotopy equivalencerelation. Isotopism is an important generalisation of isomorphism, and is studied bymathematicians in domains such as loop theory. This extension was not straightforward,and we had to solve two major technical problems, namely, generatingand verifying isotopy invariants. Concentrating on the domain of loop theory, wehave developed three novel techniques for generating isotopic invariants, by usingthe notion of universal identities and by using constructions based on subblocks.In addition, given the complexity of the theorems that verify that a conjunctionof the invariants form an isotopy class, we have developed ways of simplifying theproblem of proving these theorems. Our techniques employ an interplay of computeralgebra,model generation, theorem proving, and satisfiability-solvingmethods. To demonstrate the power of theapproach, we generate isotopic classificationtheorems for loops of size 6 and 7, which extend the previously known enumerationresults. This work was previously beyond the capabilities of automated reasoning techniques.

Original languageEnglish
Pages (from-to)221-243
Number of pages23
JournalJournal of Automated Reasoning
Volume40
Issue number2-3
DOIs
Publication statusPublished - Mar 2008
Externally publishedYes

Keywords

  • Automated mathematics
  • Automated theorem proving
  • Classification theorems
  • Computer algebra
  • Invariant generation
  • Isotopy
  • Model generation
  • SAT solving

Cite this