Comparing approaches to the exploration of the domain of residue classes. (English) Zbl 1038.68110
Summary: We report on a case study on combining proof planning with computer algebra systems. We construct proofs for basic algebraic properties of residue classes as well as for isomorphisms between residue classes using different proof techniques, which are implemented as strategies in a multi-strategy proof planner. The search space of the proof planner can be drastically reduced by employing computations of two computer algebra systems during the planning process. To test the effectiveness of our approach we carried out a large number of experiments and also compared it with some alternative approaches. In particular, we experimented with substituting computer algebra by model generation and by proving theorems with a first-order equational theorem prover instead of a proof planner.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68W30 | Symbolic computation and algebraic computation |
References:
| [1] | C. et al., Benzmüller, Proceedings of CADE-14, LNAI1249, 1997, Springer; C. et al., Benzmüller, Proceedings of CADE-14, LNAI1249, 1997, Springer |
| [2] | A. Bundy, Proceedings of CADE-9, LNCS310, 1988, Springer; A. Bundy, Proceedings of CADE-9, LNCS310, 1988, Springer |
| [3] | Fujita, M.; Slaney, J.; Bennett, F., Automatic generation of some results in finite algebra, Proceedings of IJCAI’93 (1993), Morgan Kaufmann |
| [4] | GAP, GAP—Groups, Algorithms, and Programming, Version 4; GAP, GAP—Groups, Algorithms, and Programming, Version 4 |
| [5] | Gomes, C.; Selman, B.; Kautz, H., Boosting combinatorial search through randomization, Proceedings of AAAI-98 (1998), AAAI Press |
| [6] | T. Hillenbrand, A. Jaeger, B. Löchner, Proceedings of CADE-16, LNAI1632, 1999, Springer; T. Hillenbrand, A. Jaeger, B. Löchner, Proceedings of CADE-16, LNAI1632, 1999, Springer |
| [7] | P. Jackson, Proceedings of CADE-12, LNCS814, 1994, Springer; P. Jackson, Proceedings of CADE-12, LNCS814, 1994, Springer |
| [8] | Kapur, D.; Wang, D.eds, J. Autom. Reasoning—Special on the Integration of Deduction and Symbolic Computation Systems (1998), Kluwer Academic Publisher |
| [9] | Kerber, M.; Kohlhase, M.; Sorge, V., Integrating computer algebra into proof planning, J. Autom. Reasoning, 21, 327-355 (1998) · Zbl 0916.68144 |
| [10] | W. W. McCune, Argonne National Laboratory, USA, 1994a; W. W. McCune, Argonne National Laboratory, USA, 1994a |
| [11] | W. W. McCune, Argonne National Laboratory, Argonne, IL 60439, USA, 1994b; W. W. McCune, Argonne National Laboratory, Argonne, IL 60439, USA, 1994b |
| [12] | A. Meier, 2000, Randomization and heavy-tailed behavior in proof planning. Seki Report SR-00-03, Fachbereich Informatik. Universität des Saarlandes, Saarbrücken, Germany; A. Meier, 2000, Randomization and heavy-tailed behavior in proof planning. Seki Report SR-00-03, Fachbereich Informatik. Universität des Saarlandes, Saarbrücken, Germany |
| [13] | Meier, A.; Sorge, V., Exploring properties of residue classes, Proceedings of the Calculemus Symposium 2000 (2001), AK Peters · Zbl 0986.68132 |
| [14] | A. Meier, M. Pollet, V. Sorge, 2000, Exploring the domain of residue classes. Seki Report SR-00-04, Fachbereich Informatik. Universität des Saarlandes, Saar brücken, Germany; A. Meier, M. Pollet, V. Sorge, 2000, Exploring the domain of residue classes. Seki Report SR-00-04, Fachbereich Informatik. Universität des Saarlandes, Saar brücken, Germany · Zbl 1038.68110 |
| [15] | A. Meier, M. Pollet, V. Sorge, Proceedings of EuroCAST 2001, LNCS2178, 2001, Springer; A. Meier, M. Pollet, V. Sorge, Proceedings of EuroCAST 2001, LNCS2178, 2001, Springer |
| [16] | E. Melis, A. Meier, Proceedings of the First International Conference on Computational Logic, LNAI1861, 2000, Springer; E. Melis, A. Meier, Proceedings of the First International Conference on Computational Logic, LNAI1861, 2000, Springer |
| [17] | Melis, E.; Siekmann, J., Knowledge-based proof planning, Artif. Intell., 115, 65-105 (1999) · Zbl 0939.68822 |
| [18] | Redfern, D., The Maple Handbook: Maple V Release 5 (1999), Springer · Zbl 0838.68061 |
| [19] | Robinson, J., A machine-oriented logic based on the resolution principle, JACM, 12, 23-41 (1965) · Zbl 0139.12303 |
| [20] | Slaney, J.; Fujita, M.; Stickel, M., Automated reasoning and exhaustive search: quasigroup existence problems, Comput. Math. Appl., 29, 115-132 (1995) · Zbl 0827.20083 |
| [21] | V. Sorge, Frontiers of Combining Systems: Third International Workshop, FroCoS 2000, LNCS1794, 2000, Springer; V. Sorge, Frontiers of Combining Systems: Third International Workshop, FroCoS 2000, LNCS1794, 2000, Springer |
| [22] | J. Zhang, H. Zhang, Proceedings of CADE-13, LNAI1104, 1996, Springer; J. Zhang, H. Zhang, Proceedings of CADE-13, LNAI1104, 1996, Springer |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
