MSc Project Proposal: PRESS in IsaPlanner

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.

Challenging. It will require significant programming.

• [1] Solving symbolic equations with press by Leon Sterling, Alan Bundy, Lawrence Byrd, Richard O'Keefe and Bernard Silver. In Computer Algebra, Volume 144, LNCS, 1982.
• [2] Isabelle: http://www.cl.cam.ac.uk/research/hvg/Isabelle/
• [3] The PRESS System: http://dream.inf.ed.ac.uk/software/press/
• [4] IsaPlanner: http://isaplanner.sourceforge.net/