Say no to case analysis: automating the drudgery of case-based proofs

DOI10.1007/978-3-030-79121-6_2zbMath1495.68126OpenAlexW3176533159MaRDI QIDQ2117657

Jeffrey O. Shallit

Publication date: 22 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-79121-6_2

zbMATH Keywords

algorithmautomatadecision procedurecase-based proof

Mathematics Subject Classification ID

Combinatorics on words (68R15) Formal languages and automata (68Q45) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computer assisted proofs of proofs-by-exhaustion type (68V05)

Uses Software

• Walnut

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the least number of palindromes contained in an infinite word
• Logic and \(p\)-recognizable sets of integers
• On nonrepetitive sequences
• Additive number theory via automata theory
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Composition and orbits of language operations: finiteness and upper bounds
• Every positive integer is a sum of three palindromes
• Sums of Palindromes: an Approach via Automata
• Least Periods of Factors of Infinite Words
• Every Planar Map is Four Colorable
• Decision procedure for indefinite hypergeometric summation
• A Sequence Without Repeats on x, x -1 , y, y -1
• Proofs from THE BOOK