Mechanical analysis of finite idempotent relations
Article
Kammueller, F. 2011. Mechanical analysis of finite idempotent relations. Fundamenta Informaticae. 107 (1), pp. 43-65. https://doi.org/10.3233/FI-2011-392
Type | Article |
---|---|
Title | Mechanical analysis of finite idempotent relations |
Authors | Kammueller, F. |
Abstract | We use the technique of interactive theorem proving to develop the theory and anenumeration 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 theo- retical 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. |
Research Group | Artificial Intelligence group |
Foundations of Computing group | |
Publisher | IOS Press |
Journal | Fundamenta Informaticae |
ISSN | 0169-2968 |
Electronic | 1875-8681 |
Publication dates | |
2011 | |
Publication process dates | |
Deposited | 06 Jan 2011 |
Output status | Published |
Copyright Statement | With thanks to IOS Press for permission for allowing the post-refereed article to be included. |
Digital Object Identifier (DOI) | https://doi.org/10.3233/FI-2011-392 |
Language | English |
File |
https://repository.mdx.ac.uk/item/83114
Download files
64
total views12
total downloads2
views this month1
downloads this month