Recurrence-Driven Summations in Automated Deduction

Nummelin, Visa ; Blanchette, Jasmin und Dahmen, Sander R. (2023): Recurrence-Driven Summations in Automated Deduction. 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20–22, 2023. Sattler, Uli und Suda, Martin (eds.) : In: Frontiers of Combining Systems : 14th International Symposium, FroCoS 2023 Prague, Czech Republic, September 20–22, 2023 Proceedings, Vol. 14279 Cham: Springer. pp. 23-40

Abstract

Many problems in mathematics and computer science involve summations. We present a procedure that automatically proves equations involving finite summations, inspired by the theory of holonomic sequences. The procedure is designed to be interleaved with the activities of a higher-order automatic theorem prover. It performs an induction and automatically solves the induction step, leaving the base cases to the theorem prover.

• Item Type: Conference or Workshop Item (Paper)
• Faculties: Mathematics, Computer Science and Statistics > Computer Science
• Subjects: 000 Computer science, information and general works > 004 Data processing computer science
• ISBN: 978-3-031-43368-9 ; 978-3-031-43369-6
• Place of Publication: Cham
• Language: English