Sciweavers

CADE
2006
Springer

Automatic Construction and Verification of Isotopy Invariants

14 years 10 months ago
Automatic Construction and Verification of Isotopy Invariants
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 sub-blocks. In addition, given the complexity of the theorems which 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 ...
Volker Sorge, Andreas Meier, Roy L. McCasland, Sim
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where CADE
Authors Volker Sorge, Andreas Meier, Roy L. McCasland, Simon Colton
Comments (0)