Recurrence-Driven Summations in Automated Deduction
Pages 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.
References
[1]
Abramov, S.A., Bronstein, M., Petkovsek, M., Schneider, C.: On rational and hypergeometric solutions of linear ordinary difference equations in *-field extensions. J. Symb. Comput. 107, 23–66 (2021)
[2]
Barbosa H, Reynolds A, El Ouraoui D, Tinelli C, and Barrett C Fontaine P Extending SMT solvers to higher-order logic Automated Deduction – CADE 27 2019 Cham Springer 35-54
[3]
Bhayat A and Reger G Peltier N and Sofronie-Stokkermans V A combinator-based superposition calculus for higher-order logic Automated Reasoning 2020 Cham Springer 278-296
[4]
Blanchette JC, Kaliszyk C, Paulson LC, and Urban J Hammering towards QED J. Formaliz. Reason. 2016 9 1 101-148
[5]
Bueso J, Gómez-Torrecillas J, and Verschoren A Bueso J, Gómez-Torrecillas J, and Verschoren A Gröbner bases for modules Algorithmic Methods in Non-Commutative Algebra: Applications to Quantum Groups 2003 Dordrecht Springer 169-202
[6]
Chyzak, F., Kauers, M., Salvy, B.: A non-holonomic systems approach to special function identities. In: Johnson, J.R., Park, H., Kaltofen, E. (eds.) Symbolic and Algebraic Computation, International Symposium, ISSAC 2009, Seoul, Republic of Korea, 29–31 July 2009, pp. 111–118. ACM (2009)
[7]
Cox DA, Little J, and O’Shea D Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra 2015 4 Cham Springer
[8]
Fajardo W, Gallego C, Lezama O, Reyes A, Suárez H, and Venegas H Gallego C, Lezama O, Reyes A, Suárez H, and Venegas H Gröbner bases of modules Skew PBW Extensions 2020 Cham Springer 261-286
[9]
Gosper RW Decision procedure for indefinite hypergeometric summation Proc. Natl. Acad. Sci. USA 1978 75 1 40-42
[10]
Kandri-Rody A and Weispfenning V Non-commutative Gröbner bases in algebras of solvable type J. Symb. Comput. 1990 9 1 1-26
[11]
Koutschan C Advanced applications of the holonomic systems approach ACM Comm. Comput. Algebra 2009 43 3/4 119
[12]
Ludwig M and Waldmann U Dershowitz N and Voronkov A An extension of the Knuth-Bendix ordering with LPO-Like properties Logic for Programming, Artificial Intelligence, and Reasoning 2007 Heidelberg Springer 348-362
[13]
Maletzky, A., Immler, F.: Gröbner bases of modules and Faugère’s f algorithm in Isabelle/HOL. CoRR abs/1805.00304 (2018)
[14]
Nummelin, V., Blanchette, J., Dahmen, S.R.: Automated deduction with recurrence-driven summations (technical report). Technical report (2023). https://lean-forward.github.io/pubs/sums_report.pdf
[15]
Schneider C Symbolic summation assists combinatorics Sem. Lothar. Combin. 2007 56 1-36
[16]
Steen A and Benzmüller C Extensional higher-order paramodulation in Leo-III J. Autom. Reason. 2021 65 6 775-807
[17]
Vukmirović P, Bentkamp A, Blanchette J, Cruanes S, Nummelin V, and Tourret S Making higher-order superposition work J. Autom. Reason. 2022 66 4 541-564
[18]
Vukmirović P, Blanchette J, and Schulz S Sankaranarayanan S and Sharygina N Extending a high-performance prover to higher-order logic TACAS 2023 2023 Cham Springer 111-129
[19]
Wilf HS and Zeilberger D Rational functions certify combinatorial identities J. Am. Math. Soc. 1990 3 1 147-158
[20]
Zeilberger D A holonomic systems approach to special functions identities J. Comput. Appl. Math. 1990 32 3 321-368
Recommendations
Automated Deduction in Gödel Logic
This article addresses the deduction problem of a formula from a countable theory in the first-order Gödel logic. We generalise the well-known hyperresolution principle for deduction in Gödel logic. Our approach is based on translation of a formula to ...
Peirce's rule in natural deduction
In stark contrast to Natural Deduction for Intuitionistic Logic, Natural Deduction for Classical Logic suffers from some well-known limitations: although normalisation can be proved, the standard proof of Prawitz (Natural deduction. A proof Theoretical ...
First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice
AbstractWe discuss the practical results obtained by the first generation of automated theorem provers based on Deduction modulo theory. In particular, we demonstrate the concrete improvements such a framework can bring to first-order theorem provers with ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sep 2023
281 pages
© The Author(s) 2023.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 20 September 2023
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 26 Sep 2024
Other Metrics
Citations
View Options
View options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in