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.
Original language | English |
---|---|
Title of host publication | Frontiers of Combining Systems |
Subtitle of host publication | 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20–22, 2023, Proceedings |
Editors | Uli Sattler, Martin Suda |
Place of Publication | Cham |
Publisher | Springer Science and Business Media Deutschland GmbH |
Pages | 23-40 |
Number of pages | 18 |
ISBN (Electronic) | 9783031433696 |
ISBN (Print) | 9783031433689 |
DOIs | |
Publication status | Published - 2023 |
Event | 14th International Symposium on Frontiers of Combining Systems, FroCoS 2023 - Prague, Czech Republic Duration: 20 Sept 2023 → 22 Sept 2023 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 14279 LNAI |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 14th International Symposium on Frontiers of Combining Systems, FroCoS 2023 |
---|---|
Country/Territory | Czech Republic |
City | Prague |
Period | 20/09/23 → 22/09/23 |
Bibliographical note
Funding Information:We thank Pascal Fontaine for his ideas on how to integrate our procedure into SMT and tableaux. We also thank Anne Baanen, Pascal Fontaine, Mark Summerfield, and the anonymous reviewers for suggesting improvements. Nummelin and Blanchette’s research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Dahmen’s research has received funding from the NWO under the Vidi program (project No. 639.032.613, New Diophantine Directions).
Publisher Copyright:
© 2023, The Author(s).
Funding
Nummelin and Blanchette’s research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Dahmen’s research has received funding from the NWO under the Vidi program (project No. 639.032.613, New Diophantine Directions).
Funders | Funder number |
---|---|
Nederlandse Organisatie voor Wetenschappelijk Onderzoek | 016, 639.032.613 |