Computer algebra meets automated theorem proving: Integrating maple and PVS

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

Computer algebra meets automated theorem proving: Integrating maple and PVS

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

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 - 14th International Conference, TPHOLs 2001, Proceedings
Editors	Richard J. Boulton, Paul B. Jackson
Publisher	Springer-Verlag
Pages	27-42
Number of pages	16
ISBN (Print)	354042525X, 9783540425250
Publication status	Published - 1 Jan 2001
Event	14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001 - Edinburgh, United Kingdom Duration: 3 Sept 2001 → 6 Sept 2001

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2152
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001
Country/Territory	United Kingdom
City	Edinburgh
Period	3/09/01 → 6/09/01

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, Proceedings (pp. 27-42). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2152). Springer-Verlag.

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, Proceedings. editor / Richard J. Boulton ; Paul B. Jackson. Springer-Verlag, 2001. pp. 27-42 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{415c4eab706c4e96b1050bc110a69dea,

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",

month = jan,

day = "1",

language = "English",

isbn = "354042525X",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer-Verlag",

pages = "27--42",

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

booktitle = "Theorem Proving in Higher Order Logics - 14th International Conference, TPHOLs 2001, Proceedings",

address = "Germany",

note = "14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001 ; Conference date: 03-09-2001 Through 06-09-2001",

}

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, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2152, Springer-Verlag, pp. 27-42, 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001, Edinburgh, United Kingdom, 3/09/01.

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, Proceedings. ed. / Richard J. Boulton; Paul B. Jackson. Springer-Verlag, 2001. p. 27-42 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2152).

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

TY - GEN

T1 - Computer algebra meets automated theorem proving

T2 - 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001

AU - Adams, Andrew

AU - Dunstan, Martin

AU - Gottliebsen, Hanne

AU - Kelsey, Tom

AU - Martin, Ursula

AU - Owre, Sam

PY - 2001/1/1

Y1 - 2001/1/1

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.

UR - http://www.scopus.com/inward/record.url?scp=84949506475&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:84949506475

SN - 354042525X

SN - 9783540425250

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 27

EP - 42

BT - Theorem Proving in Higher Order Logics - 14th International Conference, TPHOLs 2001, Proceedings

A2 - Boulton, Richard J.

A2 - Jackson, Paul B.

PB - Springer-Verlag

Y2 - 3 September 2001 through 6 September 2001

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, Proceedings. Springer-Verlag. 2001. p. 27-42. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Computer algebra meets automated theorem proving: Integrating maple and PVS

Abstract

Publication series

Conference

Other files and links

Fingerprint

Cite this