|MRG home page - Research - Publications - Software - People|
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.