AI4FM

Using AI to aid automation of proof search in Formal Methods

ProofProcess framework

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.

Prototype implementations are available for Isabelle (via Isabelle/Eclipse) and Z/EVES (via CZT + Z/EVES).

Download

The ProofProcess framework is currently based on the Eclipse platform. To install the latest nightly build of ProofProcess plug-ins, use the following URL as the update site:

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.