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.:

Some of these can be done using externally-computed certificates, e.g.:

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.

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.
Manuel Eberl, email {eberlm} AT []
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT []