Employing Theory Formation to Guide Proof Planning

  • Andreas Meier
  • Volker Sorge
  • Simon Colton
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2385)


The invention of suitable concepts to characterise mathematical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present an approach where automatic concept formation is used to guide non-isomorphism proofs in the residue class domain. The main idea behind the proof is to automatically identify discriminants for two given structures to show that they are not isomorphic. Suitable discriminants are generated by a theory formation system; the overall proof is constructed by a proof planner with the additional support of traditional automated theorem provers and a computer algebra system.


Production Rule Computer Algebra System Residue Class Control Rule Multiplication Table 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann, and V. Sorge. ωMega: Towards a Mathematical Assistant. In Proceedings of the 14th International Conference on Automated Deduction (CADE-14), volume 1249 of LNAI, pages 252–255. Springer Verlag, Germany, 1997.Google Scholar
  2. 2.
    A. Bundy. The Use of Explicit Plans to Guide Inductive Proofs. In Proceedings of the 9th International Conference on Automated Deduction (CADE-9), volume 310 of LNCS, pages 111–120. Springer Verlag, Germany, 1988.CrossRefGoogle Scholar
  3. 3.
    S. Colton. Automated Theory Formation in Pure Mathematics. PhD thesis, Department of Artificial Intelligence, University of Edinburgh, 2000.Google Scholar
  4. 4.
    S. Colton. An application-based comparison of automated theory formation and inductive logic programming. Linkoping Electronic Articles in Computer and Information Science (special issue: Proceedings of Machine Intelligence 17), forthcoming, 2002.Google Scholar
  5. 5.
    S. Colton, A Bundy, and T Walsh. On the notion of interestingness in automated mathematical discovery. International Journal of Human Computer Studies, 53(3):351–375, 2000.zbMATHCrossRefGoogle Scholar
  6. 6.
    S. Colton, A. Bundy, and T. Walsh. Automatic identification of mathematical concepts. In Proceedings of the 17th International Conference on Machine Learning (ICML2000), pages 183–190. Morgan Kaufmann, USA, 2001.Google Scholar
  7. 7.
    S. Colton, S Cresswell, and A Bundy. The use of classification in automated mathematical concept formation. In Proceedings of SimCat 1997: An Interdisciplinary Workshop on Similarity and Categorisation. University of Edinburgh, 1997.Google Scholar
  8. 8.
    The GAP Group, Aachen, St Andrews. GAP-Groups, Algorithms, and Programming, Version 4, 1998.
  9. 9.
    A. Meier. Tramp: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level. In Proceedings of the 17th International Conference on Automated Deduction (CADE-17), volume 1831 of LNAI, pages 460–464. Springer Verlag, Germany, 2000.Google Scholar
  10. 10.
    A. Meier, M. Pollet, and V. Sorge. Classifying Isomorphic Residue Classes. In Proceedings of the 8th International Workshop on Computer Aided Systems Theory (EuroCAST 2001), volume 2178 of LNCS, pages 494–508. Springer Verlag, Germany, 2001.CrossRefGoogle Scholar
  11. 11.
    A. Meier, M. Pollet, and V. Sorge. Comparing Approaches to Explore the Domain of Residue Classes. Journal of Symbolic Computations, 2002. forthcoming.Google Scholar
  12. 12.
    A. Meier and V. Sorge. Exploring Properties of Residue Classes. In Proceedings of the CALCULEMUS-2000 Symposium, pages 175–190. AK Peters, USA, 2001.Google Scholar
  13. 13.
    E. Melis and A. Meier. Proof planning with multiple strategies. In Proceedings of the First International Conference on Computational Logic, volume 1861 of LNAI. Springer Verlag, Germany, 2000.Google Scholar
  14. 14.
    E. Melis and J. Siekmann. Knowledge-Based Proof Planning. Artificial Intelligence, 115(1):65–105, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    S. Muggleton. Inverse entailment and Progol. New Generation Computing, 13:245–286, 1995.CrossRefGoogle Scholar
  16. 16.
    D. Redfern. The Maple Handbook: Maple V Release 5. Springer Verlag, Germany, 1999.Google Scholar
  17. 17.
    J. Zhang and H. Zhang. SEM: a System for Enumerating Models. In Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI), pages 298–303. Morgan Kaufmann, USA, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Andreas Meier
    • 1
  • Volker Sorge
    • 2
  • Simon Colton
    • 3
  1. 1.Fachbereich InformatikUniversität des SaarlandesGermany
  2. 2.School of Computer ScienceUniversity of BirminghamUK
  3. 3.Division of InformaticsUniversity of EdinburghUK

Personalised recommendations