# Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS

- Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom
Kelsey, Ursula Martin, and Sam Owre
- Theorem Proving in Higher Order Logics, TPHOLs 2001

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

PDF

### BibTeX Entry

@inproceedings{Maple-PVS:TPHOLS01,
AUTHOR = {Andrew Adams and Martin Dunstan and Hanne Gottliebsen
and Tom Kelsey and Ursula Martin and Sam Owre},
TITLE = {Computer Algebra Meets Automated Theorem Proving:
Integrating {Maple} and {PVS}},
BOOKTITLE = {Theorem Proving in Higher Order Logics, TPHOLs 2001},
EDITOR = {Richard J. Boulton and Paul B. Jackson},
PAGES = {27--42},
MONTH = sep,
YEAR = 2001,
PUBLISHER = {Springer-Verlag},
ADDRESS = {Edinburgh, Scotland},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 2152
}

Sam Owre:
owre@csl.sri.com