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

DOI10.1007/978-3-030-79121-6_2MaRDI QIDQ2117657zbMATH OpenOpenAlexFDO

Authors Jeffrey 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

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

Cites work

• scientific article; zbMATH DE number 872231 (Why is no real title available?)
• scientific article; zbMATH DE number 2235059 (Why is no real title available?)
• A Sequence Without Repeats on x, x -1 , y, y -1
• Additive number theory via automata theory
• Composition and orbits of language operations: finiteness and upper bounds
• Decision procedure for indefinite hypergeometric summation
• Distribution of Wythoff sequences modulo one
• Every Planar Map is Four Colorable
• Every positive integer is a sum of three palindromes
• Lagrange's theorem for binary squares
• Least Periods of Factors of Infinite Words
• Logic and p-recognizable sets of integers
• On nonrepetitive sequences
• On the least number of palindromes contained in an infinite word
• Proofs from THE BOOK
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Sums of Palindromes: an Approach via Automata
• What is \dots a Wilf-Zeilberger pair?

Describes a project that uses

Uses Software

• Walnut

This page was built for publication: Say no to case analysis: automating the drudgery of case-based proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2117657)