Transcript Making Conjectures About Maple Functions

Making Conjectures About
Maple Functions
Simon Colton
Universities of Edinburgh & York
Computation, Invention & Deduction
•
•
•
•
Perform calculations (CAS)
Find conjectures (ML)
Prove theorems (ATP)
Paul Zeitz, Hungarian maths contest
–
–
–
–
k = n(n+1)(n+2)(n+3), k is never a square
“Plug and chug” with n=1, n=2, n=3, n=4, ….
Gives: 24, 120, 360, 840, ….
Always square minus 1
General Approach
• Ideal world:
– ATP proves a theorem found by ML about
CAS functions
• Problem with this:
– CAS functions are too complex for ATP
• Positive spin: ATP proves from 1st principles
– Proven conjectures are likely to be less interesting
– Use ATP to discard dull results
– Find conjectures, not theorems for CAS user
Systems Used
• Maple
– Well known CAS system
• HR
– Not so well known ATF system (ML)
• Otter
– Well known ATP system
• Domain
– Number theory
The HR System – Concepts
• Automated theory formation
– Invent concepts, make conjecture, prove theorems
– Disprove non-theorems and present results
• Concept formation via 10 production rules
– Builds new concepts from old ones
– Example on next slide
• Heuristic search
– Interestingness measures (e.g., complexity)
– Limits on the concepts formed (e.g., arity, comp)
Concept Formation
[a] : isprime(a)
[a,b] : sigma(a)=b
compose
[a,b] : sigma(a)=b & isprime(b)
exists
[a] exists b (sigma(a)=b & isprime(b))
(Complexity = 4)
The HR System - Conjectures
• HR Makes conjectures empirically
– Two concepts are equivalence
– A concept is inconsistent with the axioms
– Examples of one concept all examples of another
• Extracts simpler concepts from these
– A & B & C <=> D & E
– A & B & C => D, D & E => A, etc.
• Finds prime implicates: A & B => D
• Also makes applicability conjectures
– tau(x) = x only true (empirically) for x = 1 and x = 2
Presentation of Results
• HR has some limited theorem proving
– To discard the very dull conjectures:
– f(a) & g(a)  g(a) & f(a), f(a)=b & f(a)=c [bc]
– But we didn’t want to re-invent the wheel
• HR can re-write definitions
–  b (tau(a)=b & isprime(b)) becomes isprime(tau(a))
• HR can also sort the conjectures (interestingness)
– Applicability = number of entities with non-empty examples
• Conjs about primes score 10/30 for applic (10 primes between 1 & 30)
– Surprisingness (see next slide)
Measuring Surprisingness
Surprisingness = 6
HR Using Maple
• User chooses the Maple functions of interest
• HR calls Maple to supply initial data
– User specifies initial input, say, numbers 1 to 10
– E.g., tau(10) = 4, sigma(6) = 12, etc.
• HR also calls Maple during theory formation
– HR invents concept: tau(sigma(n))
– Needs value for: tau(sigma(10)) = tau(18) = 6
– Also to find counterexamples to conjectures
• Integration via files (sorry Jürgen, MWeb soon)
HR Using Otter
• Problem with HR – too many conjectures (thesis:6%)
• Normally HR supplies Otter with only:
– Axioms of domain and the conjecture statement
• Problematic example
– All a (a=1 or a=2 => tau(a) = a)
– True but dull
– HR supplies tau(1) = 1 and tau(2) = 2 to Otter
• User can identify “axioms” to give to Otter
– E.g., isprime(a)  tau(a) = 2
• User specifies which conjs to add as axioms
– HR re-proves (and discards) many previous results
Experiment
• Aims:
– (i) show HR works with Maple
– (ii) Show pruning of conjectures works
• Three Maple functions chosen:
– tau(n), sigma(n), isprime(n)
• HR given number 1 only, but access to 2-30
• Breadth first search ran to completion
– Complexity limit of 6 and some arity constraints
• Then the user steps in
– To specify obvious results to add as axioms
• Any proven results ignored
Results
• 378 theory formation steps, approx. 2 mins
• HR called Maple 120 times
– E.g., for 195 = sigma(72) = sigma(sigma(30))
– Numbers 2, 3, 4, 5, 6, 9 and 16 introduced
• Produced 137 implicate conjectures
– 43 already proven by Otter (goodbye)
– E.g: all a ((sigma(a)=1 & sigma(1)=a) => (a=1))
• We looked through the remaining 94
– Added 9 from the first 10 (ordered by complex.)
– E.g: [3] all a ((isprime(a)) => (tau(a)=2))
– Added another 3 which were “instantiations”
• After re-proving 94 became just 22
Results Continued
• We ordered the 22 by (applic + surp)/2
• Top one was:
– isprime(sigma(a)) => isprime(tau(a))
– So interesting, we proved it (generalised)
– Then we added it as an “axiom”
• Reduced the results down to just 10:
tau(tau(a))=a => tau(sigma(sigma(a)))=sigma(a)
tau(tau(a))=a => tau(sigma(a))=a [should’ve gone]
• Are these results interesting ???
Conclusions
• Aims:
– HR works with Maple 
• No problem with the interface
– HR uses Otter to prune dull conjectures 
• 137 => 94 => 82 => 22 => 17 => 16 => 10
• Bonus: interesting conjecture(s)
• Question: is this of use to CAS users?
Further Work
• Improved pruning of conjectures
– Use Otter’s Knuth Bendix completion (McCasland)
– HR now has skolemised repn (discards exists conjs)
• Get ATF embedded in CAS (any offers?)
• Apply HR to more discovery tasks
– Roy McCasland and Zariski spaces
• Last line of my thesis:
“… if this technology can be embedded into computer algebra systems, we believe
theory formation programs will one day be important tools for mathematicians.”
Acknowledgments
• This work has been supported by
– EPSRC grant GR/M98012
– EU IHP grant:
• Calculemus HPRN-CT-2000-00102
• This work inspired by collaboration with:
– Jacques Calmet and Clemens Ballarin
– Calculemus YVR at Karlsruhe