Hidden verification for computational mathematics

H Gottliebsen; Thomas William Kelsey; U Martin

doi:10.1016/j.jsc.2004.12.005

Hidden verification for computational mathematics

H Gottliebsen, Thomas William Kelsey, U Martin

Research output: Contribution to journal › Article › peer-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. (c) 2005 Elsevier Ltd. All rights reserved.

Original language	English
Pages (from-to)	539-567
Number of pages	29
Journal	Journal of Symbolic Computation
Volume	39
Issue number	5
DOIs	https://doi.org/10.1016/j.jsc.2004.12.005
Publication status	Published - May 2005

Keywords

computer algebra
automated reasoning
real analysis

Access to Document

10.1016/j.jsc.2004.12.005

Cite this

@article{e6102ebc3cb84a2b9867d6ddad6b4195,

title = "Hidden verification for computational mathematics",

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. (c) 2005 Elsevier Ltd. All rights reserved.",

keywords = "computer algebra, automated reasoning, real analysis",

author = "H Gottliebsen and Kelsey, {Thomas William} and U Martin",

year = "2005",

month = may,

doi = "10.1016/j.jsc.2004.12.005",

language = "English",

volume = "39",

pages = "539--567",

journal = "Journal of Symbolic Computation",

issn = "0747-7171",

publisher = "Academic Press/Elsevier ",

number = "5",

}

TY - JOUR

T1 - Hidden verification for computational mathematics

AU - Gottliebsen, H

AU - Kelsey, Thomas William

AU - Martin, U

PY - 2005/5

Y1 - 2005/5

N2 - 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.

AB - 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.

KW - computer algebra

KW - automated reasoning

KW - real analysis

UR - http://www.scopus.com/inward/record.url?scp=17044431733&partnerID=8YFLogxK

UR - http://www.sciencedirect.com/science?_ob=PublicationURL&_tockey=%23TOC%236927%232005%23999609994%23592330%23FLP%23&_auth=y&view=c&_acct=C000050565&_version=1&_urlVersion=0&_userid=1026342&_pubType=J&md5=df92c1763d147a2e469ed65583590251

U2 - 10.1016/j.jsc.2004.12.005

DO - 10.1016/j.jsc.2004.12.005

M3 - Article

SN - 0747-7171

VL - 39

SP - 539

EP - 567

JO - Journal of Symbolic Computation

JF - Journal of Symbolic Computation

IS - 5

ER -

Hidden verification for computational mathematics

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

EP/C523229/1: Multidisciplinary Critical Mass in Computational Algebra and Applications

Cite this

Hidden verification for computational mathematics

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Projects

EP/C523229/1: Multidisciplinary Critical Mass in Computational Algebra and Applications

Cite this