Recurrence-Driven Summations in Automated Deduction

Visa Nummelin, Jasmin Blanchette*, Sander R. Dahmen

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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 languageEnglish
Title of host publicationFrontiers of Combining Systems
Subtitle of host publication14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20–22, 2023, Proceedings
EditorsUli Sattler, Martin Suda
Place of PublicationCham
PublisherSpringer Science and Business Media Deutschland GmbH
Pages23-40
Number of pages18
ISBN (Electronic)9783031433696
ISBN (Print)9783031433689
DOIs
Publication statusPublished - 2023
Event14th International Symposium on Frontiers of Combining Systems, FroCoS 2023 - Prague, Czech Republic
Duration: 20 Sept 202322 Sept 2023

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14279 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference14th International Symposium on Frontiers of Combining Systems, FroCoS 2023
Country/TerritoryCzech Republic
CityPrague
Period20/09/2322/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).

FundersFunder number
Nederlandse Organisatie voor Wetenschappelijk Onderzoek016, 639.032.613

    Fingerprint

    Dive into the research topics of 'Recurrence-Driven Summations in Automated Deduction'. Together they form a unique fingerprint.

    Cite this