MRG home page - Research - Publications - Software - People

University of Edinburgh

PG Tips: A Recommender System for an Interactive Theorem Prover

Project Description

Interactive theorem provers require input from users to guide the proof process. Some theorems can be complicated, making it difficult to decide which direction to take at a specific point within a proof. PG Tips is a recommender system that has been incorporated into the theorem prover Isabelle's graphical user interface, Proof General, in order to assist users.

Recommender systems are used, in a variety of situations, to provide predictions based on information supplied by a user. In this case, PG Tips is used to suggest possible proof steps based on the analysis of previous proofs. It is hoped that the creation of such a system will help users in finding proofs and accelerate the proof process.


The following people are working on the project:



To install PG Tips download PGTips.tar.gz.

You must then decompress and unpack the file using the following command

Instructions on how to use the system are available here.


Webpage maintained by Alison Mercer