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 (Hrsg.): In: Frontiers of Combining Systems : 14th International Symposium, FroCoS 2023 Prague, Czech Republic, September 20–22, 2023 Proceedings, Bd. 14279 Cham: Springer. S. 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.

• Dokumententyp: Konferenzbeitrag (Paper)
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISBN: 978-3-031-43368-9 ; 978-3-031-43369-6
• Ort: Cham
• Sprache: Englisch