Kanovich, Max A note on rewriting proofs and Fibonacci numbers. (English) Zbl 1133.05006 Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 284-292 (2007). Summary: One basic activity in combinatorics is to establish combinatorial identities by so-called ‘bijective proofs,’ which amounts to constructing explicit bijections between two types of the combinatorial objects in question. The aim of this paper is to show how techniques from the formal logic world can be applied directly to such problems studied completely independently in the world of combinatorics. The basic idea is to characterize equinumerous partition ideals in terms of the minimal elements generating the order filters, the complements to the original ideals. For the case where the minimal elements of each of these order filters are disjoint, we have developed a general automated method to remove the mystery of certain known results and establish new results in the theory of integer partitions: M. Kanovich [“Finding direct partition bijections by two-directional rewriting techniques”, Discrete Math. 285, No. 1–3, 151–166 (2004; Zbl 1044.05010 )], and M. Kanovich [“The two-way rewriting in action: Removing the mystery of Euler-Glaisher’s map”, Discrete Math. 307, No. 15, 1909–1935 (2007; Zbl 1124.05007)]. Here we address the case of filters having overlapping minimal elements. Essentially this is a case study related to the Fibonacci numeration system. In addition to a ‘bijective proof’ for Zeckendorf’s theorem – that every positive integer is uniquely representable within the Fibonacci numeration system – we establish ‘bijective proofs’ for a new series of partition identities related to Fibonacci and Lucas numbers. The main result is proved using the idea of filter supports, and rewriting systems on multisets having overlapping patterns. The main technical step is a suitable construction of such a rewriting system and then a proof that this rewriting system and the system consisting of its reverse rewriting rules, both have the Church-Rosser property, with providing the bijections we are looking for.For the entire collection see [Zbl 1121.03005]. Cited in 1 Document MSC: 05A17 Combinatorial aspects of partitions of integers 05A20 Combinatorial inequalities 68Q42 Grammars and rewriting systems 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:multiset rewriting; Church-Rosser property; confluence; termination; strong normalization; combinatorics; integer partitions; partition identities; Fibonacci numbers Citations:Zbl 1044.05010; Zbl 1124.05007 PDFBibTeX XMLCite \textit{M. Kanovich}, Lect. Notes Comput. Sci. 4514, 284--292 (2007; Zbl 1133.05006) Full Text: DOI