Back to Search
Start Over
Lagrange's Theorem for Binary Squares
- Publication Year :
- 2018
- Publisher :
- Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany, 2018.
-
Abstract
- We show how to prove theorems in additive number theory using a decision procedure based on finite automata. Among other things, we obtain the following analogue of Lagrange's theorem: every natural number > 686 is the sum of at most 4 natural numbers whose canonical base-2 representation is a binary square, that is, a string of the form xx for some block of bits x. Here the number 4 is optimal. While we cannot embed this theorem itself in a decidable theory, we show that stronger lemmas that imply that the theorem can be embedded in decidable theories, and show how automated methods can be used to search for these stronger lemmas.
- Subjects :
- FOS: Computer and information sciences
000 Computer science, knowledge, general works
Mathematics - Number Theory
Formal Languages and Automata Theory (cs.FL)
010201 computation theory & mathematics
010102 general mathematics
Computer Science
FOS: Mathematics
Computer Science - Formal Languages and Automata Theory
Number Theory (math.NT)
0102 computer and information sciences
0101 mathematics
01 natural sciences
Subjects
Details
- Language :
- English
- Database :
- OpenAIRE
- Accession number :
- edsair.doi.dedup.....2ea405179e89e5c792c18ba963fdca17
- Full Text :
- https://doi.org/10.4230/lipics.mfcs.2018.18