Abstract
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 proving techniques, which are implemented as strategies in a multi-strategy proof planner. We show how these techniques help to successfully derive proofs in our domain and explain how the search space of the proof planner can be drastically reduced by employing computations of two computer algebra systems during the planning process. Moreover, we discuss the results of experiments we conducted which give evidence that with the help of the computer algebra systems the planner is able to solve problems for which it would fail to create a proof otherwise.
The author’s work was supported by the ‘Graduiertenförderung des Saarlandes’.
The author’s work was supported by the’ studienstiftung des Deutschen Volkes’.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Bundy. The Use of Explicit Plans to Guide Inductive Proofs. In Proceedings of CADE-9, volume 310 of LNCS. Springer, 1988.
C. Benzmüuller et al. ΩMega: Towards a Mathematical Assistant. In Proceedings of CADE-14, volume 1249 of LNAI. Springer, 1997.
E. Melis et al. ActiveMath system description. In Artificial Intelligence and Education, 2001.
M. Fujita, J. Slaney, and F. Bennett. Automatic generation of some results in finite algebra. In Proceedings of IJCAI’93. Morgan Kaufmann, 1993.
The GAP Group. GAP-Groups, Algorithms, and Programming, Version 4, 1998. http://www-gap.dcs.st-and.ac.uk/~{gap}.
C. Gomes, B. Selman, and H. Kautz. Boosting combinatorial search through randomization. In Proceedings of AAAI-98. AAAI Press, 1998.
P. Jackson. Exploring Abstract Algebra in Constructive Type Theory. In Proceedings of CADE-12, volume 814 of LNCS. Springer, 1994.
D. Kapur and D. Wang, editors. Journal of Automated Reasoning— Special Issue on the Integration of Deduction and Symbolic Computation Systems, volume 21(3). Kluwer Academic Publisher, 1998.
M. Kerber, M. Kohlhase, and V. Sorge. Integrating Computer Algebra Into Proof Planning. Journal of Automated Reasoning, 21(3), 1998.
W. McCune. Otter 3.0 Reference Manual and Guide. Technical Report ANL-94-6, Argonne National Laboratory, Argonne, IL, USA, 1994.
A. Meier. Randomization and heavy-tailed behavior in proof planning. Seki Report SR-00-03, Fachbereich Informatik, Universität des Saarlandes, 2000.
A. Meier, M. Pollet, and V. Sorge. Exploring the domain of residue classes. Seki Report SR-00-04, Fachbereich Informatik, Universitäat des Saarlandes, 2000.
A. Meier and V. Sorge. Exploring Properties of Residue Classes. In Proceedings of Calculemus 2000. AK Peters, 2001.
E. Melis and A. Meier. Proof planning with multiple strategies. In Proc. of the First International Conference on Computational Logic. Springer, 2000.
E. Melis and J. Siekmann. Knowledge-based proof planning. Artificial Intelligence, 115(1), 1999.
D. Redfern. The Maple Handbook: Maple V Release 5. Springer, 1999.
J. Slaney, M. Fujita, and M. Stickel. Automated reasoning and exhaustive search: Quasigroup existence problems. Computers and Mathematics with Applications, 29, 1995.
V. Sorge. Non-Trivial Computations in Proof Planning. In Proceedings of FroCoS 2000, volume 1794 of LNCS. Springer, 2000.
Z. Zilic and K. Radecka. On feasible multivariate polynomial interpolations over arbitrary fields. In Proceedings of ISSAC-99. ACM Press, 1999.
R. Zippel. Interpolating polynomials from their values. Journal of Symbolic Computation, 9(3), 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meier, A., Pollet, M., Sorge, V. (2001). Classifying Isomorphic Residue Classes. In: Moreno-Díaz, R., Buchberger, B., Luis Freire, J. (eds) Computer Aided Systems Theory — EUROCAST 2001. EUROCAST 2001. Lecture Notes in Computer Science, vol 2178. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45654-6_39
Download citation
DOI: https://doi.org/10.1007/3-540-45654-6_39
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42959-3
Online ISBN: 978-3-540-45654-4
eBook Packages: Springer Book Archive