Automatic construction and verification of isotopy invariants

Volker Sorge, Andreas Meier, Roy McCasland, Simon Colton

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

2 Citations (Scopus)

Abstract

We extend our previous study of the automatic construction of isomorphic classification theorems for algebraic domains by considering the isotopy equivalence relation, which is of more importance than isomorphism in certain domains. This extension was not straight-forward, 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 substructures. 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 intricate interplay of computer algebra, model generation, theorem proving and satisfiability solving methods. To demonstrate the power of the approach, we generate an isotopic classification theorem for loops of size 6, which extends the previously known result that there are 22. This result was previously beyond the capabilities of automated reasoning techniques.

Original languageEnglish
Title of host publicationAutomated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings
PublisherSpringer-Verlag London Ltd.
Pages36-51
Number of pages16
ISBN (Print)3540371877, 9783540371878
Publication statusPublished - 1 Jan 2006
Externally publishedYes
EventThird International Joint Conference on Automated Reasoning, IJCAR 2006 - Seattle, WA, United States of America
Duration: 17 Aug 200620 Aug 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4130 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceThird International Joint Conference on Automated Reasoning, IJCAR 2006
CountryUnited States of America
CitySeattle, WA
Period17/08/0620/08/06

Cite this

Sorge, V., Meier, A., McCasland, R., & Colton, S. (2006). Automatic construction and verification of isotopy invariants. In Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings (pp. 36-51). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4130 LNAI). Springer-Verlag London Ltd..