An Ina Jo® proof manager for the formal development method
Daniel M. Berry · ACM SIGSOFT Software Engineering Notes · 1985
This paper describes methods for decomposing large conjectures into smaller ones in order to make their proof easier and for limiting the amount of reproving that occurs when a specification is modified. It proposes a tool, based on these methods, for managing the proofs of conjectures about an evolving specification.