Automatic Construction and Verification of Isotopy Invariants |
| |
Authors: | Volker Sorge Andreas Meier Roy McCasland Simon Colton |
| |
Affiliation: | (1) School of Computer Science, University of Birmingham, Birmingham, UK;(2) DFKI GmbH, Saarbrücken, Germany;(3) School of Informatics, University of Edinburgh, Edinburgh, UK;(4) Department of Computing, Imperial College London, London, UK |
| |
Abstract: | We extend our previous study of the automatic construction of isomorphic classification theorems for algebraic domains by
considering the isotopy equivalence relation. Isotopism is an important generalisation of isomorphism, and is studied by mathematicians in domains
such as loop theory. This extension was not straightforward, and we had to solve two major technical problems, namely, generating
and verifying isotopy invariants. Concentrating on the domain of loop theory, we have developed three novel techniques for
generating isotopic invariants, by using the notion of universal identities and by using constructions based on subblocks.
In addition, given the complexity of the theorems that verify that a conjunction of the invariants form an isotopy class,
we have developed ways of simplifying the problem of proving these theorems. Our techniques employ an interplay of computer
algebra, model generation, theorem proving, and satisfiability-solving methods. To demonstrate the power of the approach,
we generate isotopic classification theorems for loops of size 6 and 7, which extend the previously known enumeration results.
This work was previously beyond the capabilities of automated reasoning techniques.
The author’s work was supported by EPSRC MathFIT grant GR/S31099. |
| |
Keywords: | Automated mathematics Automated theorem proving SAT solving Computer algebra Model generation Isotopy Invariant generation Classification theorems |
本文献已被 SpringerLink 等数据库收录! |
|