| Title:
|
Classification results in quasigroup and loop theory via a combination of automated reasoning tools (English) |
| Author:
|
Sorge, Volker |
| Author:
|
Colton, Simon |
| Author:
|
McCasland, Roy |
| Author:
|
Meier, Andreas |
| Language:
|
English |
| Journal:
|
Commentationes Mathematicae Universitatis Carolinae |
| ISSN:
|
0010-2628 (print) |
| ISSN:
|
1213-7243 (online) |
| Volume:
|
49 |
| Issue:
|
2 |
| Year:
|
2008 |
| Pages:
|
319-339 |
| . |
| Category:
|
math |
| . |
| Summary:
|
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. (English) |
| Keyword:
|
quasigroups |
| Keyword:
|
loops |
| Keyword:
|
classification |
| Keyword:
|
automated reasoning |
| MSC:
|
20N05 |
| MSC:
|
68T15 |
| MSC:
|
68W30 |
| MSC:
|
81T05 |
| idZBL:
|
Zbl 1192.20062 |
| idMR:
|
MR2426896 |
| . |
| Date available:
|
2009-05-05T17:11:38Z |
| Last updated:
|
2013-09-22 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/119726 |
| . |
| Reference:
|
[1] Alur R., Peled D.: Computer Aided Verification.16$^{th}$ International Conference, CAV 2004, vol. 3114 of {LNCS}, Springer, Boston, MA, 2004. Zbl 1056.68003, MR 2164798 |
| Reference:
|
[2] Barrett C., Berezin S.: CVC Lite: A new implementation of the cooperating validity checker.in Alur and Peled 1, pp. 515-518. Zbl 1103.68605 |
| Reference:
|
[3] Colton S.: Automated Theory Formation in Pure Mathematics.Springer, 2002. |
| Reference:
|
[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. |
| Reference:
|
[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. Zbl 1126.68562, MR 2140374 |
| Reference:
|
[6] Colton S., Muggleton S.: Mathematical applications of inductive logic programming.Machine Learning 64 (2006), 25-64. Zbl 1103.68438, 10.1007/s10994-006-8259-x |
| Reference:
|
[7] Falconer E.: Isotopy invariants in quasigroups.Trans. Amer. Math. Society 151 (1970), 511-526. Zbl 0209.04701, MR 0272932, 10.1090/S0002-9947-1970-0272932-4 |
| Reference:
|
[8] Ganzinger H., Hagen G., Nieuwenhuis R., Oliveras A., Tinelli C.: DPLL(T): Fast decision procedures.in Alur and Peled 1, pp. 175-188. Zbl 1103.68616, MR 2164816 |
| Reference:
|
[9]
: The GAP Group.GAP - Groups, Algorithms, and Programming, Version 4.3, 2002, http://www.gap-system.org. Zbl 0319.10044 |
| Reference:
|
[10] Kronecker L.: Auseinandersetzung einiger Eigenschaften der Klassenanzahl idealer komplexer Zahlen.Monatsbericht der Berliner Akademie, pp. 881-889, 1870. |
| Reference:
|
[11] McCune W.: Mace4 Reference Manual and Guide.Argonne National Laboratory, 2003. ANL/MCS-TM-264. |
| Reference:
|
[12] McCune W.: Otter 3.3 Reference Manual.Technical Report ANL/MCS-TM-263, Argonne National Laboratory, 2003. |
| Reference:
|
[13] Meier A., Sorge V.: Applying SAT solving in classification of finite algebras.J. Automat. Reason. 35 1-3 (2005), 201-235. Zbl 1109.68103, MR 2270355 |
| Reference:
|
[14] Mitchell T.: Machine Learning.McGraw Hill, New York, 1997. Zbl 0913.68167 |
| Reference:
|
[15] Moskewicz M., Madigan C., Zhao Y., Zhang L., Malik S.: Chaff: Engineering an efficient SAT solver.in Proc. of the 39$^{th}$ Design Automation Conference (DAC 2001), Las Vegas, 2001, pp. 530-535. |
| Reference:
|
[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. Zbl 0988.68607, MR 2064587 |
| Reference:
|
[17] Schulz S.: E: A Brainiac theorem prover.Journal of AI Communication 15 2-3 (2002), 111-126. Zbl 1020.68084 |
| Reference:
|
[18] Slaney J.: FINDER, Notes and Guide.Center for Information Science Research, Australian National University, 1995. |
| Reference:
|
[19] Slaney J., Fujita M., Stickel M.: Automated reasoning and exhaustive search: Quasigroup existence problems.Comput. Math. Appl. 29 (1995), 115-132. Zbl 0827.20083, MR 1314247, 10.1016/0898-1221(94)00219-B |
| Reference:
|
[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. MR 2354671 |
| Reference:
|
[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. Zbl 1072.68596, MR 2050385 |
| Reference:
|
[22] Zhang J., Zhang H.: SEM User's Guide.Department of Computer Science, University of Iowa, 2001. |
| . |
