作者
Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula Martin, Sam Owre
发表日期
2001
研讨会论文
Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001 Edinburgh, Scotland, UK, September 3–6, 2001 Proceedings 14
页码范围
27-42
出版商
Springer Berlin Heidelberg
简介
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.
引用总数
学术搜索中的文章
A Adams, M Dunstan, H Gottliebsen, T Kelsey, U Martin… - Theorem Proving in Higher Order Logics: 14th …, 2001