Hidden Verification for Computational Mathematics

Hanne Gottliebsen, Tom Kelsey, Ursula Martin

Research output: Contribution to journalArticlepeer-review

Abstract

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.
Original languageEnglish
Pages (from-to)539-567
Number of pages29
JournalJournal of Symbolic Computation
Volume39
Issue number5
DOIs
Publication statusPublished - 1 May 2005

Keywords

  • Automated reasoning
  • Computer algebra
  • Real analysis

Fingerprint

Dive into the research topics of 'Hidden Verification for Computational Mathematics'. Together they form a unique fingerprint.

Cite this