Abstract
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.
The author’s work is supported by EPSRC grant GR/M98012 and European Union IHP grant CALCULEMUS HPRN-CT-2000-00102. He is also affiliated with the Department of Computer Science at the University of York.
This is a preview of subscription content, log in via an institution to check access.
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
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.
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.
S. Colton. Automated Theory Formation in Pure Mathematics. PhD thesis, Department of Artificial Intelligence, University of Edinburgh, 2000.
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.
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.
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.
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.
The GAP Group, Aachen, St Andrews. GAP-Groups, Algorithms, and Programming, Version 4, 1998. http://www-gap.dcs.st-and.ac.uk/~gap.
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.
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.
A. Meier, M. Pollet, and V. Sorge. Comparing Approaches to Explore the Domain of Residue Classes. Journal of Symbolic Computations, 2002. forthcoming.
A. Meier and V. Sorge. Exploring Properties of Residue Classes. In Proceedings of the CALCULEMUS-2000 Symposium, pages 175–190. AK Peters, USA, 2001.
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.
E. Melis and J. Siekmann. Knowledge-Based Proof Planning. Artificial Intelligence, 115(1):65–105, 1999.
S. Muggleton. Inverse entailment and Progol. New Generation Computing, 13:245–286, 1995.
D. Redfern. The Maple Handbook: Maple V Release 5. Springer Verlag, Germany, 1999.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meier, A., Sorge, V., Colton, S. (2002). Employing Theory Formation to Guide Proof Planning. In: Calmet, J., Benhamou, B., Caprotti, O., Henocque, L., Sorge, V. (eds) Artificial Intelligence, Automated Reasoning, and Symbolic Computation. AISC Calculemus 2002 2002. Lecture Notes in Computer Science(), vol 2385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45470-5_25
Download citation
DOI: https://doi.org/10.1007/3-540-45470-5_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43865-6
Online ISBN: 978-3-540-45470-0
eBook Packages: Springer Book Archive