Name
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. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1007/3-540-44755-5_4 | Theorem Proving in Higher Order Logics |
Keywords | Field | DocType |
real analysis library,maple users access,theorem proving,proof strategy,integrating maple,genuine symbolic computation problem,computer algebra meets automated,maple computer algebra system,real analysis,checkable proof environment,pvs automated theorem prover,symbolic computation,computer algebra,theorem prover,automated theorem proving | Maple,Prototype Verification System,Computer science,Automated theorem proving,Symbolic computation,Algorithm,Real analysis,Mathematical proof,Initial value problem | Conference |
Volume | ISBN | Citations |
2152 | 3-540-42525-X | 20 |
PageRank | References | Authors |
0.95 | 11 | 6 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andrew Adams | 1 | 936 | 53.55 |
| Martin Dunstan | 2 | 35 | 2.26 |
| Hanne Gottliebsen | 3 | 38 | 3.77 |
| Tom Kelsey | 4 | 339 | 22.24 |
| Ursula Martin | 5 | 20 | 0.95 |
| Sam Owre | 6 | 1323 | 104.39 |