Article
Full entry |
PDF
(0.3 MB)
Feedback
PDF
(0.3 MB)
Feedback
Keywords:
quasigroups; loops; classification; automated reasoning
quasigroups; loops; classification; automated reasoning
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.
References:
[1] Alur R., Peled D.: Computer Aided Verification. 16$^{th}$ International Conference, CAV 2004, vol. 3114 of {LNCS}, Springer, Boston, MA, 2004. MR 2164798 | Zbl 1056.68003
[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
[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. MR 2140374 | Zbl 1126.68562
[6] Colton S., Muggleton S.: Mathematical applications of inductive logic programming. Machine Learning 64 (2006), 25-64. DOI 10.1007/s10994-006-8259-x | Zbl 1103.68438
[7] Falconer E.: Isotopy invariants in quasigroups. Trans. Amer. Math. Society 151 (1970), 511-526. DOI 10.1090/S0002-9947-1970-0272932-4 | MR 0272932 | Zbl 0209.04701
[8] Ganzinger H., Hagen G., Nieuwenhuis R., Oliveras A., Tinelli C.: DPLL(T): Fast decision procedures. in Alur and Peled 1, pp. 175-188. MR 2164816 | Zbl 1103.68616
[9]
The GAP Group. GAP - Groups, Algorithms, and Programming, Version 4.3, 2002, http://www.gap-system.org Zbl 0319.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. MR 2270355 | Zbl 1109.68103
[14] Mitchell T.: Machine Learning. McGraw Hill, New York, 1997. Zbl 0913.68167
[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.
[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. MR 2064587 | Zbl 0988.68607
[17] Schulz S.: E: A Brainiac theorem prover. Journal of AI Communication 15 2-3 (2002), 111-126. Zbl 1020.68084
[18] Slaney J.: FINDER, Notes and Guide. Center for Information Science Research, Australian National University, 1995.
[19] Slaney J., Fujita M., Stickel M.: Automated reasoning and exhaustive search: Quasigroup existence problems. Comput. Math. Appl. 29 (1995), 115-132. DOI 10.1016/0898-1221(94)00219-B | MR 1314247 | Zbl 0827.20083
[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
[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. MR 2050385 | Zbl 1072.68596
[22] Zhang J., Zhang H.: SEM User's Guide. Department of Computer Science, University of Iowa, 2001.
Search
Partner of
