Lucas DixonTeaching → Project: PRESS in IsaPlanner

MSc Project Proposal: PRESS in IsaPlanner

Possible supervisors: Lucas Dixon, Alan Bundy

Principal goal of the project:

To port techniques from the PRESS system to IsaPlanner and Isabelle.


PRESS (PRolog Equation Solving System) is a system for solving symbolic, transcendental, non-differential equations. The methods used for solving equations are described, together with the service facilities. The principal technique, meta-level inference, appears to have applications in the broader field of symbolic and algebraic manipulation.


Knowledge of ML is beneficial. It is also strongly suggested that the student have taken the automated reasoning course and essential that they have some experience in functional programming.

Degree of Difficulty:

Challenging. It will require significant programming.