License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2018.18
URN: urn:nbn:de:0030-drops-96003
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9600/
Go to the corresponding LIPIcs Volume Portal

Madhusudan, P. ; Nowotka, Dirk ; Rajasekaran, Aayush ; Shallit, Jeffrey

Lagrange's Theorem for Binary Squares

pdf-format:
LIPIcs-MFCS-2018-18.pdf (0.4 MB)

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 the theorem can be embedded in decidable theories, and show how automated methods can be used to search for these stronger lemmas.

BibTeX - Entry

@InProceedings{madhusudan_et_al:LIPIcs:2018:9600,
  author =	{P. Madhusudan and Dirk Nowotka and Aayush Rajasekaran and Jeffrey Shallit},
  title =	{{Lagrange's Theorem for Binary Squares}},
  booktitle =	{43rd International Symposium on Mathematical Foundations  of Computer Science (MFCS 2018)},
  pages =	{18:1--18:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Igor Potapov and Paul Spirakis and James Worrell},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9600},
  URN =		{urn:nbn:de:0030-drops-96003},
  doi =		{10.4230/LIPIcs.MFCS.2018.18},
  annote =	{Keywords: binary square, theorem-proving, finite automaton, decision procedure, decidable theory, additive number theory}
}

Keywords: binary square, theorem-proving, finite automaton, decision procedure, decidable theory, additive number theory
Collection: 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)
Issue Date: 2018
Date of publication: 27.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI