MRG home page - Research - Publications - Software - People

University of Edinburgh

PG Tips: A Recommender System for an Interactive Theorem Prover

System Instructions

PG Tips is an additional feature that has been incorporated into Proof General to further assist user-interaction with interactive proof assistants. It is a recommender system that helps ease the proof process by suggesting possible proof steps based on the analysis of previous proofs. Currently, PG Tips is only available for use with Isabelle proofs.

Screenshot

    NOTE: Place use "recommender.ml"; at the top of the theory file, below the theory definition. The correct format is shown above.

  1. Use the Next or Goto buttons, situated within the toolbar, to highlight the steps the recommendations are to be based on.

  2. Select the Recmdtn button to gain recommendations for the highlighted steps.
  3. NOTE: It is advised that the display is set to three pane mode when using PG Tips, as shown above. Use Three Panes can be selected from the menu (Proof-General > Options > Display).

  4. Suggested steps can be inserted into the proof by left-clicking on them.

Back to PG Tips Home


Webpage maintained by Alison Mercer