ID: 1311.4776

A Case Study in Meta-AUTOMATION: AUTOMATIC Generation of Congruence AUTOMATA For Combinatorial Sequences

November 19, 2013

View on ArXiv

Similar papers 2

Using the "Freshman's Dream" to Prove Combinatorial Congruences

June 10, 2016

86% Match
Moa Apagodu, Doron Zeilberger
Combinatorics

In a recent beautiful but technical article, William Y.C. Chen, Qing-Hu Hou, and Doron Zeilberger developed an algorithm for finding and proving congruence identities (modulo primes) of indefinite sums of many combinatorial sequences, namely those (like the Catalan and Motzkin sequences) that are expressible in terms of constant terms of powers of Laurent polynomials. We first give a leisurely exposition of their elementary but brilliant approach, and then extend it in two di...

Find SimilarView on arXiv

On Discovering Interesting Combinatorial Integer Sequences

February 9, 2023

85% Match
Martin Svatoš, Peter Jung, Jan Tóth, ... , Kuželka Ondřej
Logic in Computer Science
Combinatorics

We study the problem of generating interesting integer sequences with a combinatorial interpretation. For this we introduce a two-step approach. In the first step, we generate first-order logic sentences which define some combinatorial objects, e.g., undirected graphs, permutations, matchings etc. In the second step, we use algorithms for lifted first-order model counting to generate integer sequences that count the objects encoded by the first-order logic formulas generated ...

Find SimilarView on arXiv

Enumeration Schemes And (More Importantly) Their Automatic Generation

May 27, 1998

85% Match
Doron Zeilberger
Combinatorics

It is way too soon to teach our computers how to become full-fledged humans. It is even premature to teach them how to become mathematicians, it is even unwise, at present, to teach them how to become combinatorialists. But the time is ripe to teach them how to become experts in a suitably defined and narrowly focused subarea of combinatorics. In this article, I will describe my efforts to teach my beloved computer, Shalosh B. Ekhad, how to be an enumerator of Wilf classes.

Find SimilarView on arXiv

On congruence schemes for constant terms and their applications

May 20, 2022

85% Match
Armin Straub
Number Theory
Combinatorics

Rowland and Zeilberger devised an approach to algorithmically determine the modulo $p^r$ reductions of values of combinatorial sequences representable as constant terms (building on work of Rowland and Yassawi). The resulting $p$-schemes are systems of recurrences and, depending on their shape, are classified as automatic or linear. We revisit this approach, provide some additional details such as bounding the number of states, and suggest a third natural type of scheme that ...

Find SimilarView on arXiv

Tree Automata

September 21, 2015

85% Match
Ferenc Gécseg, Magnus Steinby
Formal Languages and Automat...

This is a reissue of the book Tree Automata by F. G\'ecseg and M. Steinby originally published in 1984 by Akad\'emiai Kiad\'o, Budapest. Some mistakes have been corrected and a few obscure passages have been clarified. Moreover, some more recent contributions and current lines of research are reviewed in an appendix that also contains several new references.

Find SimilarView on arXiv

A Mathematical Benchmark for Inductive Theorem Provers

April 6, 2023

85% Match
Thibault Gauthier, Chad E. Brown, ... , Urban Josef
Logic in Computer Science

We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different programs generating the same OEIS sequence. Such programs were conjectured by a learning-guided synthesis system using a language with looping operators. The operators implement recursion, and thus many of the proofs require induction on natural numbers. The benchmark contains problems of varying diff...

Find SimilarView on arXiv

Congruence Relations for B\"uchi Automata

April 8, 2021

85% Match
Yong Li, Yih-Kuen Tsay, Andrea Turrini, ... , Zhang Lijun
Formal Languages and Automat...

We revisit here congruence relations for B\"uchi automata, which play a central role in the automata-based verification. The size of the classical congruence relation is in $3^{\mathcal{O}(n^2)}$, where $n$ is the number of states of a given B\"uchi automaton $\mathcal{A}$. Here we present improved congruence relations that can be exponentially coarser than the classical one. We further give asymptotically optimal congruence relations of size $2^{\mathcal{O}(n \log n)}$. Base...

Find SimilarView on arXiv

A Congruence-Based Perspective on Finite Tree Automata

April 23, 2021

85% Match
Pierre Ganty, Elena Gutiérrez, Pedro Valero
Formal Languages and Automat...

We provide new insights on the determinization and minimization of tree automata using congruences on trees. From this perspective, we study a Brzozowski's style minimization algorithm for tree automata. First, we prove correct this method relying on the following fact: when the automata-based and the language-based congruences coincide, determinizing the automaton yields the minimal one. Such automata-based congruences, in the case of word automata, are defined using pre and...

Find SimilarView on arXiv

Mechanical Proofs of Properties of the Tribonacci Word

July 22, 2014

84% Match
Hamoon Mousavi, Jeffrey Shallit
Formal Languages and Automat...
Discrete Mathematics
Combinatorics

We implement a decision procedure for answering questions about a class of infinite words that might be called (for lack of a better name) "Tribonacci-automatic". This class includes, for example, the famous Tribonacci word T = 0102010010202 ..., the fixed point of the morphism 0 -> 01, 1 -> 02, 2 -> 0. We use it to reprove some old results about the Tribonacci word from the literature, such as assertions about the occurrences in T of squares, cubes, palindromes, and so forth...

Find SimilarView on arXiv

A Method of Verifying Partition Congruences by Symbolic Computation

April 5, 2020

84% Match
Cristian-Silviu Radu, Nicolas Allen Smoot
Number Theory

Conjectures involving infinite families of restricted partition congruences can be difficult to verify for a number of individual cases, even with a computer. We demonstrate how the machinery of Radu's algorithm may be modified and employed to efficiently check a very large number of cases of such conjectures. This allows substantial evidence to be collected for a given conjecture, before a complete proof is attempted.

Find SimilarView on arXiv