Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS

Andrew Adams; Martin Dunstan; Hanne Gottliebsen; Tom Kelsey; Ursula Martin; Sam Owre

doi:10.1007/3-540-44755-5_4

Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS

Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula Martin, Sam Owre

School of Informatics

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

Abstract

We describe an interface between version 6 of the Maple computer algebra system with the PVS automated theorem prover. The interface is designed to allow Maple users access to the robust and checkable proof environment of PVS. We also extend this environment by the provision of a library of proof strategies for use in real analysis. We demonstrate examples using the interface and the real analysis library. These examples provide proofs which are both illustrative and applicable to genuine symbolic computation problems.

Original language	English
Title of host publication	Theorem Proving in Higher Order Logics
Subtitle of host publication	14th International Conference, TPHOLs 2001 Edinburgh, Scotland, UK, September 3–6, 2001 Proceedings
Editors	Richard J. Boulton, Paul B. Jackson
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	27-42
Number of pages	16
ISBN (Print)	978-3-540-44755-9
DOIs	https://doi.org/10.1007/3-540-44755-5_4
Publication status	Published - 2001

Publication series

Name	Lecture Notes in Computer Science
Volume	2152

Access to Document

10.1007/3-540-44755-5_4

https://link.springer.com/chapter/10.1007/3-540-44755-5_4

Cite this

Adams, A., Dunstan, M., Gottliebsen, H., Kelsey, T., Martin, U., & Owre, S. (2001). Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS. In R. J. Boulton, & P. B. Jackson (Eds.), Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001 Edinburgh, Scotland, UK, September 3–6, 2001 Proceedings (pp. 27-42). (Lecture Notes in Computer Science; Vol. 2152). Springer. https://doi.org/10.1007/3-540-44755-5_4

Adams, Andrew ; Dunstan, Martin ; Gottliebsen, Hanne et al. / Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS. Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001 Edinburgh, Scotland, UK, September 3–6, 2001 Proceedings. editor / Richard J. Boulton ; Paul B. Jackson. Berlin, Heidelberg : Springer, 2001. pp. 27-42 (Lecture Notes in Computer Science).

@inproceedings{decbbbaad4194f92b929a1f5fe5d9947,

title = "Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS",

abstract = "We describe an interface between version 6 of the Maple computer algebra system with the PVS automated theorem prover. The interface is designed to allow Maple users access to the robust and checkable proof environment of PVS. We also extend this environment by the provision of a library of proof strategies for use in real analysis. We demonstrate examples using the interface and the real analysis library. These examples provide proofs which are both illustrative and applicable to genuine symbolic computation problems.",

author = "Andrew Adams and Martin Dunstan and Hanne Gottliebsen and Tom Kelsey and Ursula Martin and Sam Owre",

year = "2001",

doi = "10.1007/3-540-44755-5_4",

language = "English",

isbn = "978-3-540-44755-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "27--42",

editor = "Boulton, {Richard J.} and Jackson, {Paul B.}",

booktitle = "Theorem Proving in Higher Order Logics",

address = "United Kingdom",

}

Adams, A, Dunstan, M, Gottliebsen, H, Kelsey, T, Martin, U & Owre, S 2001, Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS. in RJ Boulton & PB Jackson (eds), Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001 Edinburgh, Scotland, UK, September 3–6, 2001 Proceedings. Lecture Notes in Computer Science, vol. 2152, Springer, Berlin, Heidelberg, pp. 27-42. https://doi.org/10.1007/3-540-44755-5_4

Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS. / Adams, Andrew; Dunstan, Martin; Gottliebsen, Hanne et al.
Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001 Edinburgh, Scotland, UK, September 3–6, 2001 Proceedings. ed. / Richard J. Boulton; Paul B. Jackson. Berlin, Heidelberg: Springer, 2001. p. 27-42 (Lecture Notes in Computer Science; Vol. 2152).

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

TY - GEN

T1 - Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS

AU - Adams, Andrew

AU - Dunstan, Martin

AU - Gottliebsen, Hanne

AU - Kelsey, Tom

AU - Martin, Ursula

AU - Owre, Sam

PY - 2001

Y1 - 2001

N2 - We describe an interface between version 6 of the Maple computer algebra system with the PVS automated theorem prover. The interface is designed to allow Maple users access to the robust and checkable proof environment of PVS. We also extend this environment by the provision of a library of proof strategies for use in real analysis. We demonstrate examples using the interface and the real analysis library. These examples provide proofs which are both illustrative and applicable to genuine symbolic computation problems.

AB - We describe an interface between version 6 of the Maple computer algebra system with the PVS automated theorem prover. The interface is designed to allow Maple users access to the robust and checkable proof environment of PVS. We also extend this environment by the provision of a library of proof strategies for use in real analysis. We demonstrate examples using the interface and the real analysis library. These examples provide proofs which are both illustrative and applicable to genuine symbolic computation problems.

U2 - 10.1007/3-540-44755-5_4

DO - 10.1007/3-540-44755-5_4

M3 - Conference contribution

SN - 978-3-540-44755-9

T3 - Lecture Notes in Computer Science

SP - 27

EP - 42

BT - Theorem Proving in Higher Order Logics

A2 - Boulton, Richard J.

A2 - Jackson, Paul B.

PB - Springer

CY - Berlin, Heidelberg

ER -

Adams A, Dunstan M, Gottliebsen H, Kelsey T, Martin U, Owre S. Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS. In Boulton RJ, Jackson PB, editors, Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001 Edinburgh, Scotland, UK, September 3–6, 2001 Proceedings. Berlin, Heidelberg: Springer. 2001. p. 27-42. (Lecture Notes in Computer Science). doi: 10.1007/3-540-44755-5_4

Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS

Abstract

Publication series

Access to Document

Fingerprint

Cite this