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 proceedingConference contribution

Abstract / Description of output

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 languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication14th International Conference, TPHOLs 2001 Edinburgh, Scotland, UK, September 3–6, 2001 Proceedings
EditorsRichard J. Boulton, Paul B. Jackson
Place of PublicationBerlin, Heidelberg
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Print)978-3-540-44755-9
Publication statusPublished - 2001

Publication series

NameLecture Notes in Computer Science


Dive into the research topics of 'Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS'. Together they form a unique fingerprint.

Cite this