Algebraic Theory Exploration: A Comparison of Technologies

Quratul Ain Mahesar, Volker Sorge

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


We present a case study in comparing tools for theory exploration in finite algebra. Our aim is to compare experimentally diverse technologies for generating finite algebraic structures. In particular, we compare the performance of model generators, constraint solvers and satisfiability solvers in their ability to generate large algebraic structures, in our case quasigroups, that exhibit some desired property. In addition to a straight forward comparison of technologies using a number of non-trivial properties, we also experiment with techniques that further constrain the original problems by pre-computing additional information and observe its effect on the performance of different systems. We thereby use two particular constructions, one based on randomisation the other on pre-computing additional knowledge. The former filters randomly pre-computed elements by automated theorem proving to exclude unsuitable instantiations. The latter employs a concept of generating systems particularly suitable for quasigroups, that can be easily computed for small size quasigroups and evolved to be suitable for larger size structures. We present comparative experimental results to evaluate our proposed approaches in terms of increasing the solvability horizon as well as time reduction in finding the solutions for the algebraic structures with particular properties. The experimental results give us insight into the suitable selection of the systems that could benefit from the presented algebraic techniques.

Original languageEnglish
Title of host publicationSYNASC 2012
Subtitle of host publication14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
EditorsAndrei Voronkov, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, Stephen Watt, Daniela Zaharie
PublisherIEEE Computer Society
Number of pages8
ISBN (Print)9780769549347, 9781467350266
Publication statusPublished - 26 Sep 2012
Externally publishedYes
Event14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing - Timisoara, Romania
Duration: 26 Sep 201229 Sep 2012
Conference number: 14


Conference14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
Abbreviated titleSYNASC 2012


Dive into the research topics of 'Algebraic Theory Exploration: A Comparison of Technologies'. Together they form a unique fingerprint.

Cite this