PG Tips: A Recommender System for an Interactive Theorem Prover
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.