TY - GEN
T1 - PG Tips: A Recommender System for an Interactive Theorem Prover
AU - Mercer,Alison Elizabeth
AU - Bundy,Alan
AU - Duncan,Hazel
AU - Aspinall,David
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
M3 - Conference contribution
SP - 1
EP - 8
BT - Proceedings of Mathematical User-Interfaces Workshop (MathUI’2006)
ER -