Bachelors Thesis
In interactive theorem provers such as Isabelle, the system provides a collection of automatic proof methods for solving individual goals, ranging from simplifiers and classical reasoners to tableau and smt solvers. Applications of those methods require a varying amount of user input and configuration. Consequently, proofs can often be stated differently, with different run-time and cognitive complexity characteristics. Over time, proof methods evolve and become stronger, removing the need to use more complex methods. Thus, older existing formalizations frequently contain proofs that could be nowadays be made more concise.
The goal of this project is to develop a tool that alleviates that problem by automatically re-writing existing proofs, taking into account the complexity of source text, the underlying proof term as well as method run-times.
Programming language:
ML, Isar
Prerequisites:
Isabelle experience; Familiarity with ML or similar functional language; English
Advisor:
Fabian Huch, email {huch} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, email {nipkow} AT [in.tum.de]