Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Automatic Construction and Verification of Isotopy Invariants
Authors: Volker Sorge ; Andreas Meier ; Roy McCasland ; Simon Colton
Date: 2008
Publication Title:Journal of Automated Reasoning
Publication Type:Journal Article Publication Status:Published
Volume No:40 Page Nos:221-243
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.
Links To Paper
1st Link
Bibtex format
author = { Volker Sorge and Andreas Meier and Roy McCasland and Simon Colton },
title = {Automatic Construction and Verification of Isotopy Invariants},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
year = 2008,
volume = {40},
pages = {221-243},
doi = {10.1007/s10817-007-9093-y},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh