InterACT. An interactive theorem and completeness prover for algebraic specifications with conditional equations

The InterACT tool is an interactive theorem prover for algebraic specifications emphasizing user-friendliness. InterACT is integrated in the existing ACT environment. The main purpose of InterACT is to teach formal methods in universitary courses about formal specification of software systems. It has already been used successfully in this area. The theoretical and practical concepts underlying InterAcr are described in this paper. Ideas for the design of user interfaces for interactive theorem provers can be found.