Hidden verification for computational mathematics

H Gottliebsen, Thomas William Kelsey, U Martin

Research output: Contribution to journalArticlepeer-review

5 Citations (Scopus)


We present hidden verification as a means to make the power of computational logic available to users of computer algebra systems while shielding them from its complexity. We have implemented in PVS a library of facts about elementary and transcendental functions, and automatic procedures to attempt proofs of continuity, convergence and differentiability for functions in this class. These are called directly from Maple by a simple pipe-lined interface. Hence we are able to support the analysis of differential equations in Maple by direct calls to PVS for: result refinement and verification, discharge of verification conditions, harnesses to ensure more reliable differential equation solvers, and verifiable look-up tables. (c) 2005 Elsevier Ltd. All rights reserved.

Original languageEnglish
Pages (from-to)539-567
Number of pages29
JournalJournal of Symbolic Computation
Issue number5
Publication statusPublished - May 2005


  • computer algebra
  • automated reasoning
  • real analysis


Dive into the research topics of 'Hidden verification for computational mathematics'. Together they form a unique fingerprint.

Cite this