Calculational Relation-Algebraic Proofs in Isabelle/Isar

  • Wolfram Kahl
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3051)


We propose a collection of theories in the proof assistant Isabelle/Isar that support calculational reasoning in and about heterogeneous relational algebras and Kleene algebras.


Relation Algebra Proof Assistant Proof Checker Transitivity Rule Computer Science Application 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Asp00]
    Aspinall, D.: Proof General: A generic tool for proof development. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 38–42. Springer, Heidelberg (2000), See also CrossRefGoogle Scholar
  2. [BBS97]
    Behnke, R., Berghammer, R., Schneider, P.: Machine support of relational computations: The Kiel RELVIEW system. Technical Report 9711, Institut für Informatik und Praktische Mathematik, Christian- Albrechts- Universität Kiel (June 1997)Google Scholar
  3. [BH94]
    Berghammer, R., Hattensperger, C.: Computer-aided manipulation of relational expressions and formulae using RALF. In: Buth, B., Berghammer, R. (eds.) Systems for Computer-Aided Specification, Development and Verification, Bericht Nr. 9416, pp. 62–78. Universit ät Kiel (1994)Google Scholar
  4. [BHL99]
    Berghammer, R., Hoffmann, T., Leoniuk, B.: Rechnergest ützte Erstellung von Prototypen für Programme auf relationalen Strukturen. Technical Report 9905, Institut für Informatik und praktische Mathematik, Christian-Albrechts-Universität Kiel (July 1999)Google Scholar
  5. [BW01]
    Bauer, G., Wenzel, M.: Calculational reasoning revisited, an Isabelle/Isar experience. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 75–90. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. [Des03]
    Desharnais, J.: Kleene algebras with relations. In: Berghammer, R., Möller, B. (eds.) Proc. RelMiCS 7, International Seminar on Relational Methods in Computer Science, in combination with the 2nd Intl. Workshop on Applications of Kleene Algebra. LNCS, Springer, Heidelberg (2003) (Invited Talk)Google Scholar
  7. [DG00]
    Dougherty, D., Gutiérrez, C.: Normal forms and reduction for theories of binary relations. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 95–109. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  8. [DM01]
    Desharnais, J., Möller, B.: Characterizing determinacy in Kleene algebras. Information Sciences 139, 253–273 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  9. [DMS03]
    Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. Technical Report 2003-7, Universität Augsburg, Institut für Informatik (2003)Google Scholar
  10. [dS02]
    de Swart, H.C.M. (ed.): RelMiCS 2001. LNCS, vol. 2561. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  11. [FS90]
    Freyd, P.J., Scedrov, A.: Categories, Allegories. North-Holland Mathematical Library, vol. 39. North-Holland, Amsterdam (1990)zbMATHGoogle Scholar
  12. [Fur98]
    Furusawa, H.: Algebraic Formalisations of Fuzzy Relations and Their Representation Theorems. PhD thesis, Department of Informatics, Kyushu University (March 1998)Google Scholar
  13. [HBS94]
    Hattensperger, C., Berghammer, R., Schmidt, G.: RALF – A relation-algebraic formula manipulation system and proof checker. Notes to a system demonstration. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) AMAST 1993, Workshops in Computing, pp. 405–406. Springer, Heidelberg (1994)Google Scholar
  14. [Jip01]
    Jipsen, P.: Implementing quasi-equational logic on the web. In: Talk given at the AMS Sectional Meeting, University of South Carolina, March 16-18 (2001),
  15. [Jip03]
    Jipsen, P.: PCP: Point and click proofs (2003), Web-based system at
  16. [Kah01]
    Kahl, W.: A relation-algebraic approach to graph structure transformation, Habil. Thesis, Fakultät für Informatik, Univ. der Bundeswehr München, Techn. Bericht 2002-03 (2001)Google Scholar
  17. [Kah02]
    Kahl, W.: A relation-algebraic approach to graph structure transformation. In: de Swart [dS02], pp. 1–14 (Invited Talk)Google Scholar
  18. [KH98]
    Kahl, W., Hattensperger, C.: Second-order syntax in HOPS and in RALF. In: Buth, B., Berghammer, R., Peleska, J. (eds.) Tools for System Development and Verification. BISS Monographs, vol. 1, pp. 140–164. Shaker Verlag, Aachen (1998) ISBN: 3-8265- 3806-4Google Scholar
  19. [Koz91]
    Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inform. and Comput. 110(2), 366–390 (1991)CrossRefMathSciNetGoogle Scholar
  20. [Koz94]
    Kozen, D.: On action algebras. In: van Eijck, J., Visser, A. (eds.) Logic and Information Flow, pp. 78–88. MIT Press, Cambridge (1994)Google Scholar
  21. [Koz97]
    Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems, 427–443 (May 1997)Google Scholar
  22. [Koz98]
    Kozen, D.: Typed Kleene algebra. Technical Report 98-1669, Computer Science Department, Cornell University (March 1998)Google Scholar
  23. [KS00]
    Kahl, W., Schmidt, G.: Exploring (finite) Relation Algebras using Tools written in Haskell. Technical Report 2000-02, Fakultät für Informatik, Universität der Bundeswehr München (October 2000), see also the RATH page
  24. [KWP99]
    Kammüller, F., Wenzel, M., Paulson, L.C.: Locales - a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149–166. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  25. [Nip03]
    Nipkow, T.: Structured proofs in Isar/HOL. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 259–278. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  26. [NPW02]
    Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHCrossRefGoogle Scholar
  27. [SHW97]
    Schmidt, G., Hattensperger, C., Winter, M.: Heterogeneous relation algebra. In: Brink, C., Kahl, W., Schmidt, G. (eds.) Relational Methods in Computer Science, Advances in Computing Science, ch. 3, pp. 39–53. Springer, New York (1997)Google Scholar
  28. [SS93]
    Schmidt, G., Ströhlein, T.: Relations and Graphs, Discrete Mathematics for Computer Scientists. EATCS-Monographs on Theoretical Computer Science. Springer, Heidelberg (1993)zbMATHGoogle Scholar
  29. [Str02]
    Struth, G.: Calculating Church-Rosser proofs in Kleene algebra. In: de Swart [dS02], pp. 276–290Google Scholar
  30. [VB99]
    Verhoeven, R., Backhouse, R.: Towards tool support for program verification and construction. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1128–1146. Springer, Heidelberg (1999)Google Scholar
  31. [vOG97]
    von Oheimb, D., Gritzner, T.F.: RALL: Machine-supported proofs for relation algebra. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 380–394. Springer, Heidelberg (1997)Google Scholar
  32. [Wen97]
    Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 307–322. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  33. [Wen02]
    Wenzel, M.M.: Isabelle/Isar - A Versatile Environment for Human- Readable Formal Proof Documents. PhD thesis, Technische Universität München, Fakultät für Informatik (February 2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Wolfram Kahl
    • 1
  1. 1.Department of Computing and SoftwareMcMaster University 

Personalised recommendations