Bachelor Thesis or Bachelor’s/Master’s practical course.
The goal is to implement various additional tactics and/or simplification procedures (‘simprocs’) to simplify/expand certain mathematical terms that are difficult to simplify using simp rules, e.g.:
- proving/disproving/rewriting statements like “4/3 ∈ ℤ”,
- expanding ln(n) = ∑ ki ln(pi) using the prime factorisation n = ∏ pik,
- pulling out perfect k-th powers from k-th roots, e.g. sqrt(12) = 3sqrt(2) (probably again using prime factorisation)
- removing integer multiples of π/2 from the arguments of sin, cos, tan, etc.
- prime testing, prime power testing, prime factorisation
- power-freeness testing and Carmichael number testing
- k-th integer root and k-th power testing
- multiplicative function (using prime factorisation): Euler’s totient function, Möbius µ function, divisor function
Some of these can be done using externally-computed certificates, e.g.:
- primality: Pratt certificate,
- prime power: prime factor (with Pratt certificate) and multiplicity,
- compositeness: two non-trivial factors,
- non-prime-power: two non-trivial coprime factors
- prime factorisation: list of primes factors with multiplicity; Pratt certificate for each prime
- non-k-th-power-freeness: perfect k-th power factor
For the tactics (but not for the simprocs), these certificates could also be computed by an external tool (e.g. Maxima). This may require the student to write some code in Maxima as well. Otherwise, a ‘native’ certifier can be written in ML.
Proofs of concepts for some of these already exist (e.g. in the Pratt_Certificate and Bertrands_Postulate AFP entries). The goal would be to make a bigger collection of fast and robust tactics/simprocs.
Prerequisites:
The project involves little to no formalisation. Most of the work will be Isabelle/ML programming, so some familiarity with Isabelle and Standard ML would be helpful. However, there are no big technical difficulties, so the project should be feasible even for a Bachelor’s student with no knowledge of Isabelle. Good functional programming skills are, however, necessary.
Advisor:
Manuel Eberl, email {eberlm} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]