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

Laura I. Meikle; Jacques D. Fleuriot

doi:10.1007/978-3-540-85110-3_27

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

Laura I. Meikle, Jacques D. Fleuriot

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 language	English
Title of host publication	Intelligent Computer Mathematics
Subtitle of host publication	9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings
Editors	Serge Autexier, John Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki, Freek Wiedijk
Publisher	Springer Berlin Heidelberg
Pages	315-330
Number of pages	16
Volume	5144
ISBN (Electronic)	978-3-540-85110-3
ISBN (Print)	978-3-540-85109-7
DOIs	https://doi.org/10.1007/978-3-540-85110-3_27
Publication status	Published - 2008

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg

Access to Document

10.1007/978-3-540-85110-3_27

http://dx.doi.org/10.1007/978-3-540-85110-3_27

Cite this

Meikle, L. I., & Fleuriot, J. D. (2008). Combining Isabelle and QEPCAD-B in the Prover's Palette. In S. Autexier, J. Campbell, J. Rubio, V. Sorge, M. Suzuki, & F. Wiedijk (Eds.), Intelligent Computer Mathematics: 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings (Vol. 5144, pp. 315-330). (Lecture Notes in Computer Science). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-85110-3_27

Meikle, Laura I. ; Fleuriot, Jacques D. / Combining Isabelle and QEPCAD-B in the Prover's Palette. Intelligent Computer Mathematics: 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings. editor / Serge Autexier ; John Campbell ; Julio Rubio ; Volker Sorge ; Masakazu Suzuki ; Freek Wiedijk. Vol. 5144 Springer Berlin Heidelberg, 2008. pp. 315-330 (Lecture Notes in Computer Science).

@inproceedings{6110f7b982164dbc8ed193b106fa7f15,

title = "Combining Isabelle and QEPCAD-B in the Prover's Palette",

abstract = "We present the Prover{\textquoteright}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.",

author = "Meikle, {Laura I.} and Fleuriot, {Jacques D.}",

year = "2008",

doi = "10.1007/978-3-540-85110-3_27",

language = "English",

isbn = "978-3-540-85109-7",

volume = "5144",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "315--330",

editor = "Serge Autexier and John Campbell and Julio Rubio and Volker Sorge and Masakazu Suzuki and Freek Wiedijk",

booktitle = "Intelligent Computer Mathematics",

}

Meikle, LI & Fleuriot, JD 2008, Combining Isabelle and QEPCAD-B in the Prover's Palette. in S Autexier, J Campbell, J Rubio, V Sorge, M Suzuki & F Wiedijk (eds), Intelligent Computer Mathematics: 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings. vol. 5144, Lecture Notes in Computer Science, Springer Berlin Heidelberg, pp. 315-330. https://doi.org/10.1007/978-3-540-85110-3_27

Combining Isabelle and QEPCAD-B in the Prover's Palette. / Meikle, Laura I.; Fleuriot, Jacques D.

Intelligent Computer Mathematics: 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings. ed. / Serge Autexier; John Campbell; Julio Rubio; Volker Sorge; Masakazu Suzuki; Freek Wiedijk. Vol. 5144 Springer Berlin Heidelberg, 2008. p. 315-330 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Meikle, Laura I.

AU - Fleuriot, Jacques D.

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-540-85110-3_27

DO - 10.1007/978-3-540-85110-3_27

M3 - Conference contribution

SN - 978-3-540-85109-7

VL - 5144

T3 - Lecture Notes in Computer Science

SP - 315

EP - 330

BT - Intelligent Computer Mathematics

A2 - Autexier, Serge

A2 - Campbell, John

A2 - Rubio, Julio

A2 - Sorge, Volker

A2 - Suzuki, Masakazu

A2 - Wiedijk, Freek

PB - Springer Berlin Heidelberg

ER -

Meikle LI, Fleuriot JD. Combining Isabelle and QEPCAD-B in the Prover's Palette. In Autexier S, Campbell J, Rubio J, Sorge V, Suzuki M, Wiedijk F, editors, Intelligent Computer Mathematics: 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings. Vol. 5144. Springer Berlin Heidelberg. 2008. p. 315-330. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-85110-3_27

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

Abstract

Publication series

Access to Document

Fingerprint

Cite this