Combining Isabelle and QEPCAD-B in the Prover's Palette

Laura I. Meikle, Jacques D. Fleuriot

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We present the Prover’s Palette, a framework for combining mathematical tools, and describe an integration of the theorem prover Isabelle with the computer algebra system QEPCAD-B following this approach. Examples are used to show how results from QEPCAD can be used in a variety of ways, with and without trust. We include new functionality for instantiating witnesses automatically and auto-running where applicable. We conclude that user-centric design yields systems integrations which are extremely versatile and easy to use.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publication9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings
EditorsSerge Autexier, John Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki, Freek Wiedijk
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-540-85110-3
ISBN (Print)978-3-540-85109-7
Publication statusPublished - 2008

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


Dive into the research topics of 'Combining Isabelle and QEPCAD-B in the Prover's Palette'. Together they form a unique fingerprint.

Cite this