Projects per year
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 satisfiabilitysolving 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.
Original language  English 

Pages (fromto)  221243 
Number of pages  23 
Journal  Journal of Automated Reasoning 
Volume  40 
Issue number  23 
DOIs  
Publication status  Published  Mar 2008 
Keywords
 Automated mathematics
 Automated theorem proving
 SAT solving
 Computer algebra
 Model generation
 Isotopy
 Invariant generation
 Classification theorems
Fingerprint
Dive into the research topics of 'Automatic Construction and Verification of Isotopy Invariants'. Together they form a unique fingerprint.Projects
 2 Finished


Integration and Interaction of multiple mathematical reasoning processes
Bundy, A., Colton, S., Aspinall, D., Dennis, L., Fleuriot, J., Georgieva, L., Ireland, A., Jackson, P. & Smaill, A.
1/04/07 → 31/03/11
Project: Research