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

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)
Pages1-8
Number of pages8
Publication statusPublished - 2006

Fingerprint

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

Cite this