VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up

A. A. Adams, H. Gottliebsen, S. A. Linton, U. Martin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

We present a verifiable symbolic definite integral table lookup: a system which matches a query, comprising a definite integral with parameters and side conditions, against an entry in a verifiable table and uses a call to a library of facts about the reals in the theorem prover PVS to aid in the transformation of the table entry into an answer. Our system is able to obtain correct answers in cases where standard techniques implemented in computer algebra systems fail. We present the full model of such a system as well as a description of our prototype implementation showing the efficacy of such a system: for example, the prototype is able to obtain correct answers in cases where computer algebra systems [CAS] do not. We extend upon Fateman's web-based table by including parametric limits of integration and queries with side conditions.
Original languageEnglish
Title of host publicationAutomated Deduction - CADE-16
Subtitle of host publication16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings
Place of PublicationBerlin, Heidelberg
PublisherSpringer Berlin Heidelberg
Number of pages15
ISBN (Print)978-3-540-48660-2
Publication statusPublished - 1999

Publication series

NameLecture Notes in Computer Science


Dive into the research topics of 'VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up'. Together they form a unique fingerprint.

Cite this