Making conjectures about maple functions

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

5 Citations (Scopus)

Abstract

One of the main applications of computational techniques to pure mathematics has been the use of computer algebra systems to perform calculations which mathematicians cannot perform by hand. Because the data is produced within the computer algebra system, this becomes an environment for the exploration of new functions and the data produced is often analysed in order to make conjectures empirically. We add some automation to this by using the HR theory formation system to make conjectures about Maple functions supplied by the user. Experience has shown that HR produces too many conjectures which are easily proven from the definitions of the functions involved. Hence, we use the Otter theorem prover to discard any theorems which can be easily proven, leaving behind the more interesting ones which are empirically true but not trivially provable. By providing an application of HR’s theory formation in number theory, we show that using Otter to prune HR’s dull conjectures has much potential for producing interesting conjectures about standard computer algebra functions.

Original languageEnglish
Title of host publicationArtificial Intelligence, Automated Reasoning and Symbolic Computation - Joint International Conferences AISC 2002 and Calculemus 2002, Proceedings
EditorsLaurent Henocque, Jacques Calmet, Belaid Benhamou, Olga Caprotti, Volker Sorge
PublisherSpringer
Pages259-274
Number of pages16
ISBN (Print)3540438653, 9783540438656
DOIs
Publication statusPublished - 2002
Externally publishedYes
EventJoint Conferences on 6th Artificial Intelligence and Symbolic Computation, AISC 2002 and 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2002 - Marseille, France
Duration: 1 Jul 20025 Jul 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2385
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceJoint Conferences on 6th Artificial Intelligence and Symbolic Computation, AISC 2002 and 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2002
CountryFrance
CityMarseille
Period1/07/025/07/02

Cite this

Colton, S. (2002). Making conjectures about maple functions. In L. Henocque, J. Calmet, B. Benhamou, O. Caprotti, & V. Sorge (Eds.), Artificial Intelligence, Automated Reasoning and Symbolic Computation - Joint International Conferences AISC 2002 and Calculemus 2002, Proceedings (pp. 259-274). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2385). Springer. https://doi.org/10.1007/3-540-45470-5