Overview

The work mentioned here mainly concerns the sequent prover. All along the lifecycle of the prover, the following improvements can be achieved :

adding new useful proof rules (to prove sequents that are hard to prove or even not provable at all)
correcting bugs in implementations of existing proof rules
implementing new tools to help the user do proofs
evolving prover API to fit with the needs of prover plug-in developers

Motivations

Areas of improvement for provers can be summarized as follows:

reducing proving time and effort
providing the user with more efficient proving tools
- reducing proof storage space (proof purging / simplifying)
- ease manual proof review or reuse (prf skl view with copy paste)
maintain consistency / coherence / ? when correcting prover implementation (versioning)
ensure that prover modifications are well reflected by the platform

Part of implemented rules and user interface capabilities come from user feedback mainly through SourceForge feature requests. SourceForge bugs are also an important input for corrections.