Mechanical Analysis of Finite Idempotent Relations

• Autorzy: Kammüller F.
• Języki publikacji: EN

Abstrakty

EN

We use the technique of interactive theoremproving to develop the theory and an enumeration technique for finite idempotent relations. Starting from a short mathematical characterization of finite idempotents defined and proved in Isabelle/HOL, we derive first an iterative procedure to generate all instances of idempotents over a finite set. From there, we develop a more precise theoretical characterization giving rise to an efficient predicate that can be executed in the programming language ML. Idempotent relations represent a very basic, general mathematical concept but the steps taken to develop their theory with the help of Isabelle/HOL are representative for developing algorithms from a mathematical specification

Słowa kluczowe

EN

Formal Specification of Computer Systems; Idempotent Relations; Interactive Theorem Proving; Higher Order Logic

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 107, nr 1
• Strony: 43--65
• Opis fizyczny: Bibliogr. 17 poz., wykr.

Twórcy

autor

Kammüller F.

• Middlesex University, The Borroughs, NW4 4BT, London UK,

Bibliografia

• [1] G. Brinkmann and B. D.McKay Posets on up to 16 points. Order 19 (2002); no. 2, 147-179.MR 2003e:05002
• [2] J. Burghardt, F. Kammüller and J. W. Sanders. On the Antisymmetry of Galois Embeddings. Information Processing Letters, 79:2, Elsevier, June 2001.
• [3] A. H. Clifford and G. B. Preston. The Algebraic Theory of Semigroups, volume 1. Mathematical Surveys, number 7. American Mathematical Society. 1961.
• [4] C. W. Curtis and I. Reiner. Representation Theory of Finite Groups and Associative Algebras. Interscience Publishers, JohnWiley, 1966.
• [5] R. A. Davey and H. A. Priestley. Introduction to Lattices and Order, Second Edition. Cambridge University Press, 2002.
• [6] N. Dunford and J. T. Schwartz. Linear Operators. Part I: General Theory. John Wiley, 1958.
• [7] G. Engels et. al. Quasar Enterprise - Anwendungslandschaften service-orientiert gestalten. d-punkt.verlag, 2009.
• [8] F. Kammüller. http://www.swt.cs.tu-berlin.de/∼flokam.
• [9] He Jifeng, C. A. R. Hoare, J. W. Sanders Data Refinement Refined (resume). In ESOP'86, pages 187-196. Volume 213 of LNCS, Springer, 1986.
• [10] F. Kammüller. Interactive Theorem Proving in Software Engineering. (Habilitationsschrift), VDM Müller, 2007.
• [11] F. Kammüller and J. W. Sanders. Idempotent Relations in Isabelle/HOL. In First International Colloquium on Theoretical Aspects of Computing. Vol. 3407 LNCS, Springer, 2005.
• [12] F. Kammüller,M. Wenzel, and L. C. Paulson. Locales - a Sectioning Concept for Isabelle. Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99. Vol. 1690 LNCS, Springer, 1999.
• [13] L. C. Paulson. Isabelle: the Next 700 Theorem Provers. In: P. Odifreddi (editor), Logic and Computer Science, pages 361-386. Academic Press, 1990.
• [14] L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer LNCS, 828, 1994.
• [15] G. Pfeiffer. Counting Transitive Relations. Journal of Integer Sequences, 7:3, 2004.
• [16] M. Sch¨onert et al. GAP: Groups, Algorithms and Programming. RWTH Aachen, http://www.gapsystem.org
• [17] N. J. A. Sloane The on-line encyclopedia of integer sequences. Published electronically AT http://www.research.att.com/∼njas/sequences, 2003.