Classification results in quasigroup and loop theory via a combination of automated reasoning tools

Volker Sorge; Simon Colton; Roy McCasland; Andreas Meier

Commentationes Mathematicae Universitatis Carolinae (2008)

  • Volume: 49, Issue: 2, page 319-339
  • ISSN: 0010-2628

Abstract

top
We present some novel classification results in quasigroup and loop theory. For quasigroups up to size 5 and loops up to size 7, we describe a unique property which determines the isomorphism (and in the case of loops, the isotopism) class for any example. These invariant properties were generated using a variety of automated techniques --- including machine learning and computer algebra --- which we present here. Moreover, each result has been automatically verified, again using a variety of techniques --- including automated theorem proving, computer algebra and satisfiability solving --- and we describe our bootstrapping approach to the generation and verification of these classification results.

How to cite

top

Sorge, Volker, et al. "Classification results in quasigroup and loop theory via a combination of automated reasoning tools." Commentationes Mathematicae Universitatis Carolinae 49.2 (2008): 319-339. <http://eudml.org/doc/250479>.

@article{Sorge2008,
abstract = {We present some novel classification results in quasigroup and loop theory. For quasigroups up to size 5 and loops up to size 7, we describe a unique property which determines the isomorphism (and in the case of loops, the isotopism) class for any example. These invariant properties were generated using a variety of automated techniques --- including machine learning and computer algebra --- which we present here. Moreover, each result has been automatically verified, again using a variety of techniques --- including automated theorem proving, computer algebra and satisfiability solving --- and we describe our bootstrapping approach to the generation and verification of these classification results.},
author = {Sorge, Volker, Colton, Simon, McCasland, Roy, Meier, Andreas},
journal = {Commentationes Mathematicae Universitatis Carolinae},
keywords = {quasigroups; loops; classification; automated reasoning; finite quasigroups; finite loops; classification; automated reasoning; isomorphisms; isotopisms},
language = {eng},
number = {2},
pages = {319-339},
publisher = {Charles University in Prague, Faculty of Mathematics and Physics},
title = {Classification results in quasigroup and loop theory via a combination of automated reasoning tools},
url = {http://eudml.org/doc/250479},
volume = {49},
year = {2008},
}

TY - JOUR
AU - Sorge, Volker
AU - Colton, Simon
AU - McCasland, Roy
AU - Meier, Andreas
TI - Classification results in quasigroup and loop theory via a combination of automated reasoning tools
JO - Commentationes Mathematicae Universitatis Carolinae
PY - 2008
PB - Charles University in Prague, Faculty of Mathematics and Physics
VL - 49
IS - 2
SP - 319
EP - 339
AB - We present some novel classification results in quasigroup and loop theory. For quasigroups up to size 5 and loops up to size 7, we describe a unique property which determines the isomorphism (and in the case of loops, the isotopism) class for any example. These invariant properties were generated using a variety of automated techniques --- including machine learning and computer algebra --- which we present here. Moreover, each result has been automatically verified, again using a variety of techniques --- including automated theorem proving, computer algebra and satisfiability solving --- and we describe our bootstrapping approach to the generation and verification of these classification results.
LA - eng
KW - quasigroups; loops; classification; automated reasoning; finite quasigroups; finite loops; classification; automated reasoning; isomorphisms; isotopisms
UR - http://eudml.org/doc/250479
ER -

References

top
  1. Alur R., Peled D., Computer Aided Verification, 16 International Conference, CAV 2004, vol. 3114 of LNCS, Springer, Boston, MA, 2004. Zbl1056.68003MR2164798
  2. Barrett C., Berezin S., CVC Lite: A new implementation of the cooperating validity checker, in Alur and Peled 1, pp. 515-518. Zbl1103.68605
  3. Colton S., Automated Theory Formation in Pure Mathematics, Springer, 2002. 
  4. Colton S., Bundy A., Walsh T., Automatic identification of mathematical concepts, in Machine Learning: Proceedings of the 17th International Conference, 2000, pp.183-190. 
  5. Colton S., Meier A., Sorge V., McCasland R., Automatic Generation of classification theorems for finite algebras, in David Basin and Michael Rusinowitch, Eds., Automated Reasoning - 2nd International Joint Conference, IJCAR 2004, vol. 3097 of {LNAI}, Springer, Cork, Ireland, 2004, pp.400-414. Zbl1126.68562MR2140374
  6. Colton S., Muggleton S., 10.1007/s10994-006-8259-x, Machine Learning 64 (2006), 25-64. (2006) Zbl1103.68438DOI10.1007/s10994-006-8259-x
  7. Falconer E., 10.1090/S0002-9947-1970-0272932-4, Trans. Amer. Math. Society 151 (1970), 511-526. (1970) Zbl0209.04701MR0272932DOI10.1090/S0002-9947-1970-0272932-4
  8. Ganzinger H., Hagen G., Nieuwenhuis R., Oliveras A., Tinelli C., DPLL(T): Fast decision procedures, in Alur and Peled 1, pp. 175-188. Zbl1103.68616MR2164816
  9. The GAP Group, GAP - Groups, Algorithms, and Programming, Version 4.3, 2002, http://www.gap-system.org. Zbl0319.10044
  10. Kronecker L., Auseinandersetzung einiger Eigenschaften der Klassenanzahl idealer komplexer Zahlen, Monatsbericht der Berliner Akademie, pp. 881-889, 1870. 
  11. McCune W., Mace4 Reference Manual and Guide, Argonne National Laboratory, 2003. ANL/MCS-TM-264. 
  12. McCune W., Otter 3.3 Reference Manual, Technical Report ANL/MCS-TM-263, Argonne National Laboratory, 2003. 
  13. Meier A., Sorge V., Applying SAT solving in classification of finite algebras, J. Automat. Reason. 35 1-3 (2005), 201-235. (2005) Zbl1109.68103MR2270355
  14. Mitchell T., Machine Learning, McGraw Hill, New York, 1997. Zbl0913.68167
  15. Moskewicz M., Madigan C., Zhao Y., Zhang L., Malik S., Chaff: Engineering an efficient SAT solver, in Proc. of the 39 Design Automation Conference (DAC 2001), Las Vegas, 2001, pp. 530-535. 
  16. Riazanov A., Voronkov A., Vampire 1.1, in Rejeev Goré, Alexander Leitsch, and Tobias Nipkow, Eds., Automated Reasoning - 1st International Joint Conference, IJCAR 2001, vol. 2083 of {LNAI}, Springer, Siena, Italy, 2001, pp. 376-380. Zbl0988.68607MR2064587
  17. Schulz S., E: A Brainiac theorem prover, Journal of AI Communication 15 2-3 (2002), 111-126. (2002) Zbl1020.68084
  18. Slaney J., FINDER, Notes and Guide, Center for Information Science Research, Australian National University, 1995. 
  19. Slaney J., Fujita M., Stickel M., 10.1016/0898-1221(94)00219-B, Comput. Math. Appl. 29 (1995), 115-132. (1995) Zbl0827.20083MR1314247DOI10.1016/0898-1221(94)00219-B
  20. Sorge V., Meier A., McCasland R., Colton S., The automatic construction of isotopy invariants, in Third International Joint Conference on Automated Reasoning, 2006, pp.36-51. MR2354671
  21. Weidenbach C., Brahm U., Hillenbrand T., Keen E., Theobald C., Topic D., SPASS Version 2.0, in A. Voronkov, Ed., Proc. of the 18th International Conference on Automated Deduction (CADE-18), vol. 2392 of {LNAI}, Springer, Berlin, 2002, pp.275-279. Zbl1072.68596MR2050385
  22. Zhang J., Zhang H., SEM User's Guide, Department of Computer Science, University of Iowa, 2001. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.