Author | Conference | Journal | Organization | Year | DOI
Look for results that meet for the following criteria:
Academic
Publications
Automated conjecture making in number theory using HR, Otter and Maple

Automated conjecture making in number theory using HR, Otter and Maple,10.1016/j.jsc.2004.12.003,Journal of Symbolic Computation,Simon Colton

Edit
Automated conjecture making in number theory using HR, Otter and Maple   (Citations: 4)
BibTex | RIS | RefWorks Download
One of the main applications of computational techniques to pure math- ematics has been the use of computer algebra systems to perform cal- culations 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 discovery process by using the HR theory formation system to make conjectures about Maple functions supplied by the user. HR forms theories by inventing concepts, making conjectures empirically which relate the concepts, and appealing to third party theorem provers and model generators to prove/disprove the conjectures. It has been used with success in number theory, graph theory and various algebraic do- mains such as group theory and ring theory. Experience has shown that HR produces too many conjectures which can be 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 empiri- cally plausible but not easily provable. We describe the core functionality of HR which enables it to form a theory, and the additional functionality implemented in order for HR to work with Maple functions. We present two experiments where we have applied HR's theory formation in number theory. We discuss the modes of operation for the user and provide some of the results produced in this way. We hope to show that using HR, Ot- ter and Maple in this fashion has much potential for the advancement of computer algebra systems.
Journal: Journal of Symbolic Computation - JSC , vol. 39, no. 5, pp. 593-615, 2005
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
More »
    • ...For example, the ICARUS system for reformulating constraint satisfaction problems [1] and the HOMER system for conjecture making in number theory [2]...
    • ...To demonstrate the flexibility of the framework, we extended this initial configuration to applications in number theory similar to those performed by the HOMER system [2]...
    • ...Importantly, our system re-discovered the most interesting results from [2], including e.g., isprime(σ(a)) → isprime(τ (a))...

    John Charnley, et al. A Global Workspace Framework for Combining Reasoning Systems

    • ...In the HOMER system [7], HR was used in conjunction with Otter and the Maple computer algebra package [24] in order to make conjectures about computer algebra functions...
    • ...In [7], we applied this approach to number theory, using some functions which included a Boolean primality test, and τ(n) and σ(n) which calculate the number and sum of divisors of n respectively...
    • ...We ran the system to completion with a complexity limit of 6. Under a similar experimental set up, as reported in [7], HOMER created 48 concepts, whereas our configuration created 97, of which 38 were found in HOMER’ s corpus of 48. We identified four reasons why the extra ten concepts were not created by our system...

    John Charnley, et al. Applications of a Global Workspace Framework to Mathematical Discovery

Sort by:

Citations (4)

Share this on