- Developed in Java using Eclipse IDE
- Can be run on various operating systems and sever platforms
- Is designed to facilitate and standardize output formatting
Feature 1: Analysis of the Proof Structure
Easy-to-use interface:
- Enter the Isabelle/HOL directory location
- Click Analyze button, check out processing information.
- The results of analysis are presented as an Excel file
Feature 2: Optimization of the Isabelle/HOL theories
If a lemma is neither representing a top level property of the system nor used in any of the other lemmas within the provided set of theories, it can be removed from the original Isabelle theory.
Easy-to-use interface:
- In Excel file generated by the Analyzer, mark lemmas representing the top level properties with star (*) in the final sheet.
- Select Excel file updated in the previous step and the Isabelle theory to be optimized.
- Click ‘Optimize’ button and check output for optimizing log information.
- After optimization, all redundant lemmas are removed in the newly generated version of Isabelle/HOL theory file.
RMIT SUMMER PROJECTS 2016 