A framework to capture, store and analyse expert's interactive proof process. The framework is part of the AI4FM research project, which aims to learn from an expert doing interactive theorem proving to increase automation of formal proofs.
Install the ProofProcess framework plug-ins by using the following update site in the Eclipse Update Manager:
http://www.ai4fm.org/proofprocess/updates/nightly/
When installing, select the ProofProcess framework for your theorem prover, e.g. Isabelle ProofProcess integration or Z/EVES ProofProcess integration - all required plug-ins will be downloaded and installed automatically.
Note that Isabelle/Eclipse requires Java 7 to run, so make sure that your Eclipse IDE is running on Java 7. Refer to Isabelle/Eclipse documentation for details.
The framework aims to be generic across theorem provers. Current prototype implementations include support for Isabelle and Z/EVES theorem provers.
The core of the framework is currently based on the Eclipse platform. We are using EMF to model and represent the proof process. The code is developed as a mixed Java/Scala solution, therefore Scala IDE is required to build it.
Prototype implementation with Isabelle proof assistant is available. Currently it requires Isabelle/Eclipse IDE (source code available on GitHub).
The Isabelle/ProofProcess plug-ins are named org.ai4fm.proofprocess.isabelle.*.
Prototype implementation with Z/EVES proof assistant is available. The integration is based on and requires Community Z Tools (CZT) link with Z/EVES. It is available from CZT repository (not included in the official 1.5 release).
The Isabelle/ProofProcess plug-ins are named org.ai4fm.proofprocess.zeves.*.