Skip to main content
SpringerLink
Log in
Book cover

International Conference on Computer Aided Systems Theory

EUROCAST 2001: Computer Aided Systems Theory — EUROCAST 2001 pp 494–508Cite as

Classifying Isomorphic Residue Classes

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2178))

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’.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Bundy. The Use of Explicit Plans to Guide Inductive Proofs. In Proceedings of CADE-9, volume 310 of LNCS. Springer, 1988.

    Google Scholar 

  2. C. Benzmüuller et al. ΩMega: Towards a Mathematical Assistant. In Proceedings of CADE-14, volume 1249 of LNAI. Springer, 1997.

    Google Scholar 

  3. E. Melis et al. ActiveMath system description. In Artificial Intelligence and Education, 2001.

    Google Scholar 

  4. M. Fujita, J. Slaney, and F. Bennett. Automatic generation of some results in finite algebra. In Proceedings of IJCAI’93. Morgan Kaufmann, 1993.

    Google Scholar 

  5. The GAP Group. GAP-Groups, Algorithms, and Programming, Version 4, 1998. http://www-gap.dcs.st-and.ac.uk/~{gap}.

  6. C. Gomes, B. Selman, and H. Kautz. Boosting combinatorial search through randomization. In Proceedings of AAAI-98. AAAI Press, 1998.

    Google Scholar 

  7. P. Jackson. Exploring Abstract Algebra in Constructive Type Theory. In Proceedings of CADE-12, volume 814 of LNCS. Springer, 1994.

    Google Scholar 

  8. 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.

    Google Scholar 

    Google Scholar 

  9. M. Kerber, M. Kohlhase, and V. Sorge. Integrating Computer Algebra Into Proof Planning. Journal of Automated Reasoning, 21(3), 1998.

    Google Scholar 

  10. W. McCune. Otter 3.0 Reference Manual and Guide. Technical Report ANL-94-6, Argonne National Laboratory, Argonne, IL, USA, 1994.

    Google Scholar 

  11. A. Meier. Randomization and heavy-tailed behavior in proof planning. Seki Report SR-00-03, Fachbereich Informatik, Universität des Saarlandes, 2000.

    Google Scholar 

  12. 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.

    Google Scholar 

  13. A. Meier and V. Sorge. Exploring Properties of Residue Classes. In Proceedings of Calculemus 2000. AK Peters, 2001.

    Google Scholar 

  14. E. Melis and A. Meier. Proof planning with multiple strategies. In Proc. of the First International Conference on Computational Logic. Springer, 2000.

    Google Scholar 

  15. E. Melis and J. Siekmann. Knowledge-based proof planning. Artificial Intelligence, 115(1), 1999.

    Google Scholar 

  16. D. Redfern. The Maple Handbook: Maple V Release 5. Springer, 1999.

    Google Scholar 

  17. J. Slaney, M. Fujita, and M. Stickel. Automated reasoning and exhaustive search: Quasigroup existence problems. Computers and Mathematics with Applications, 29, 1995.

    Google Scholar 

  18. V. Sorge. Non-Trivial Computations in Proof Planning. In Proceedings of FroCoS 2000, volume 1794 of LNCS. Springer, 2000.

    Google Scholar 

  19. Z. Zilic and K. Radecka. On feasible multivariate polynomial interpolations over arbitrary fields. In Proceedings of ISSAC-99. ACM Press, 1999.

    Google Scholar 

  20. R. Zippel. Interpolating polynomials from their values. Journal of Symbolic Computation, 9(3), 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität des Saarlandes, Germany

    Andreas Meier, Martin Pollet & Volker Sorge

Authors
  1. Andreas Meier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Pollet
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Volker Sorge
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Universidad de Las Palmas de Gran Canaria, Instituto Universitario de Ciencias y Tecnologías Cibernéticas, Campus de Tafira, 35017, Las Palmas de Gran Canaria, Spain

    Roberto Moreno-Díaz

  2. University of Linz, Research Institute for Symbolic Computation, 232, Schloss Hagenberg, Austria

    Bruno Buchberger

  3. University ofA Coruña, Facultad de Informática, LFCIA, Dpto. of Computer Science, Campus de Elviña, 15071, A Coruña, Spain

    José Luis Freire

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation