Adams, A.A. and Gottliebsen, H. and Linton, S.A. and Martin, U. (1999) VSDITLU: a verified symbolic definite integral table look-up. In: Automated Deduction -- CADE-16 16th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, 1632 (1632). Springer-Verlag, Berlin, pp. 112-126. ISBN 3-540-66222-7
This is the latest version of this item.
![[img]](http://opendepot.org/style/images/fileicons/application_pdf.png)
| PDF Download (101Kb) | Preview |
Abstract
We present a verifiable symbolic definite integral table look-up: 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.
| Item Type: | Book Section |
|---|---|
| Subjects: | Mathematical and Computer Sciences > Others in Mathematical and Computing Sciences > Mathematical and Computing Sciences not elsewhere classified |
| Divisions: | UNSPECIFIED |
| Depositing User: | Dr Andrew Adams |
| Date Deposited: | 23 Jul 2008 14:23 |
| Last Modified: | 23 Aug 2010 14:26 |
| URI: | http://opendepot.org/id/eprint/79 |
Available Versions of this Item
- VSDITLU: a verified symbolic definite integral table look-up. (deposited 23 Jul 2008 14:23)
- VSDITLU: a verified symbolic definite integral table look-up. (deposited 23 Jul 2008 14:23)[Currently Displayed]
Actions (login required)
| View Item |
