{"references": ["[1] A. A. Adams, H. Gottliebsen, S. A. Linton, and U. Martin. A Verifiable Symbolic Definite Integral Table Look-Up. Technical Report CS/99/3, University of St Andrews, 1999. http://www-theory.cs.stand. ac.uk/publications/CAAR/CS993. [2] A. A. Adams, H. Gottliebsen, S. A. Linton, and U. Martin. Automated theorem proving in support of computer algebra: symbolic definite integration as a case study. In Dooley [7], pages 253\u00e2\ufffd\ufffd260. [3] A. A. Adams, H. Gottliebsen, S. A. Linton, and U. Martin. VSDITLU: a verifiable symbolic definite integral table look-up. In Ganzinger [9], pages 112\u00e2\ufffd\ufffd126. [4] M. Bronstein. SUM-IT: A strongly-typed embeddable computer algebra library. In Calmet and Limongelli [5]. [5] J. Calmet and C. Limongelli, editors. Design and Implementation of Symbolic Computation Systems, International Symposium, DISCO \u00e2\ufffd\ufffd96. Springer-Verlag LNCS 1128, 1996. [6] S. Dalmas, M. Ga\ufffd\u00a8etano, and C. Huchet. A Deductive Database for Mathematical Formulas. In Calmet and Limongelli [5]. [7] S. Dooley, editor. Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation. ACM Press, 1999. [8] B. Dutertre. Elements of Mathematical Analysis in PVS. In von Wright et al. [16], pages 141\u00e2\ufffd\ufffd156. [9] H. Ganzinger, editor. Automated Deduction \u00e2\ufffd\ufffd CADE-16. Springer-Verlag LNAI 1632, 1999. [10] K. O. Geddes, S. R. Czapor, and G. Labahn. Algorithms for Computer Algebra. Kluwer, 1992. [11] H. Gottliebsen. Transcendental Functions and Continuity Checking in PVS. In Harrison and Aagaard [13], pages 198\u00e2\ufffd\ufffd215. [12] I. S. Gradshteyn and I. M. Ryzhik. Table of Integrals, Series and Products. Academic Press, 1965. [13] J. Harrison and M. Aagaard, editors. Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000. Springer-Verlag LNAI 1869, 2000. [14] L. Sterling, A. Bundy, L. Byrd, R. O\u00e2\ufffd\ufffdKeefe, and B. Silver. Solving symbolic equations with PRESS. J. Symbolic Comput., 7(1):71\u00e2\ufffd\ufffd84, 1989. [15] D. Stoutemyer. Crimes and misdemeanours in the computer algebra trade. Notices of the AMS, 38:779\u00e2\ufffd\ufffd785, 1991. [16] J. von Wright, J. Grundy, and J. Harrison, editors. Theorem Proving in Higher Order Logics: 9th International Conference. Springer-Verlag LNCS 1125, 1996."]}

In [2] we presented a Definite Integral Table Lookup (the DITLU) for parametric functions, including a minimal prototype implementation demonstrating its capabilities. In this paper we present a possible application of a DITLU, which would extend its utility for a modest investment of effort. The naive algorithm for indefinite integration of rational functions (see e.g. [12, �2.10]) can be implemented for parametric rational functions. This involves splitting the rational function integrand using partial fractions. The resulting integrands all fall within a limited class which may be covered in a DITLU by a very small number of table entries. Extensions of this idea to less naive integration algorithms, and the number of table entries required to implement them, are also considered. This record was migrated from the OpenDepot repository service in June, 2017 before shutting down.