Simon Foster, Georg Struth, and Tjark Weber. In Harrie C. M. de Swart, editor, Relational and Algebraic Methods in Computer Science - 12th International Conference, RAMICS 2011, Rotterdam, The Netherlands, May 30 - June 3, 2011. Proceedings, volume 6663 of Lecture Notes in Computer Science, pages 52-67. Springer, 2011.
We present a new integration of relational and algebraic methods in the Isabelle/HOL theorem proving environment. It consists of a fine grained hierarchy of algebraic structures based on Isabelle's type classes and locales, and a repository of more than 800 facts obtained by automated theorem proving. We demonstrate further benefits of Isabelle for hypothesis learning, duality reasoning, theorem instantiation, and reasoning across models and theories. Our work forms the basis for a reference repository and a program development environment based on algebraic methods. It can also be used by mathematicians for exploring and integrating new variants.
The original publication is available at www.springerlink.com.
@inproceedings{foster11automated,
author = {Simon Foster and Georg Struth and Tjark Weber},
title = {Automated Engineering of Relational and Algebraic Methods in {Isabelle/HOL}~-- (Invited Tutorial)},
editor = {Harrie C. M. de Swart},
booktitle = {Relational and Algebraic Methods in Computer Science~-- 12th International Conference, RAMICS 2011, Rotterdam, The Netherlands, May~30~- June~3, 2011. Proceedings},
volume = {6663},
series = {Lecture Notes in Computer Science},
pages = {52--67},
publisher = {Springer},
year = {2011},
url = {http://dx.doi.org/10.1007/978-3-642-21070-9_5}
}