A page from the OpenDepot.org service

Jump to the start of the main contents

Adams, A.A. and Dunstan, M. and Gottliebsen, H. and Kelsey, T. and Martin, U. and Owre, S. (2001) Computer Algebra meets Automated Theorem Proving: Integrating Maple and PVS. In: Theorem Proving in Higher Order Logics -- 14th International Conference, TPHOLs 2001. Lecture Notes in Computer Science (2152). Springer-Verlag, Berlin, pp. 27-42. ISBN 3-540-42525-X

Download (142Kb) | Preview


    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.

    Item Type: Book Section
    Subjects: Mathematical and Computer Sciences > Others in Mathematical and Computing Sciences > Mathematical and Computing Sciences not elsewhere classified
    Divisions: UNSPECIFIED
    Depositing User: Dr Andrew Adams
    Date Deposited: 23 Jul 2008 14:23
    Last Modified: 23 Aug 2010 14:26
    URI: http://opendepot.org/id/eprint/77

    Actions (login required)

    View Item