PG Tips: A Recommender System for an Interactive Theorem Prover

Alison Elizabeth Mercer, Alan Bundy, Hazel Duncan, David Aspinall

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

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationProceedings of Mathematical User-Interfaces Workshop (MathUI’2006)
Number of pages8
Publication statusPublished - 2006


Dive into the research topics of 'PG Tips: A Recommender System for an Interactive Theorem Prover'. Together they form a unique fingerprint.

Cite this