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

  • Marcus Klar
  • Robert Geisler
  • Felix Cornelius
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1130)


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 InterACT are described in this paper. Ideas for the design of user interfaces for interactive theorem provers can be found.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Bardohl. Concept and Implementation of the Language GVT for the Graphical Visualisation of Terms of Algebraic Specifications (in german). Master's thesis, Technische Universität Berlin, 1993.Google Scholar
  2. 2.
    I. Claßen. Compositionality of Application Oriented Structuring Mechanisms for Algebraic Specification Languages with Initial Semantics. PhD thesis, Technische Universität Berlin, 1993.Google Scholar
  3. 3.
    I. Claßen, H. Ehrig, and D. Wolz. Algberaic Specification Techniques and Tools for Software Development — The ACT Approach. AMAST Series in Computing Vol. 1. World Scientific, 1993.Google Scholar
  4. 4.
    H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer, Berlin, 1985.Google Scholar
  5. 5.
    R. Geisler and M. Klar. Design and Realisation of the Interactive Theorem-and Completeness Prover InterACT for Algebraic Specifications (in german). Master's thesis, Technische Universität Berlin, June 1995.Google Scholar
  6. 6.
    M. Heisel, W. Reif, and W. Stephan. Tactical theorem proving in program verification. In 10th International Conference on Automated Deduction. Springer LNCS 449, July 1990.Google Scholar
  7. 7.
    T. Langbacka, R. Ruksenas, and J. von Wright. TkWinHOL A Tool for Doing Window Inference in HOL. Technical report, Abo Akademi University, 1995.Google Scholar
  8. 8.
    L.C. Paulson. Logic and Computation. Cambridge University Press, 1987.Google Scholar
  9. 9.
    L.C. Paulson. Isabelle. Springer LNCS 828, 1994.Google Scholar
  10. 10.
    P. Robinson and J. Staples. Formalizing a hierarchical structure of practical mathematical reasoning. Journal of Logic and Computation, 3(1), Feb. 1993.Google Scholar
  11. 11.
    J. Rumbaugh. Eine Betrachtung der Architektur Model-View-Controller (MVC) (in german). OBJEKTspektrum, 3, März 94.Google Scholar
  12. 12.
    D. Wolz. Design of a compiler for lazy pattern driven narrowing. In Proc. of the 7th International Workshop on the Specification of Abstract Data Types, LNCS 534. Springer, 1991.Google Scholar
  13. 13.
    D. Wolz. A tool for checking ADT completeness and consistency. In Proc. of the third LOTOSPHERE workshop, Pisa, 1992.Google Scholar
  14. 14.
    H. Zhang, D. Kapur, and M. S. Krishnamoorthy. A mechanizable induction prinziple for equational specifications. In E. Lusk and R. Overbeek, editors, 10th International Conference on Automated Deduction (LNCS 310). Springer, 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Marcus Klar
    • 1
  • Robert Geisler
    • 2
  • Felix Cornelius
    • 2
  1. 1.Fraunhofer-Institut für Software- und Systemtechnik ISSTBerlin
  2. 2.FB InformatikTechnische Universität BerlinBerlin

Personalised recommendations