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

}