Edinburgh Research Explorer

PG Tips: A Recommender System for an Interactive Theorem Prover

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Open Access permissions


Original languageEnglish
Title of host publicationProceedings of Mathematical User-Interfaces Workshop (MathUI’2006)
Number of pages8
Publication statusPublished - 2006


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 authoring process.

Download statistics

No data available

ID: 25105811