License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CPM.2022.2
URN: urn:nbn:de:0030-drops-161297
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16129/
Shallit, Jeffrey
Using Automata and a Decision Procedure to Prove Results in Pattern Matching (Invited Talk)
Abstract
The first-order theory of automatic sequences with addition is decidable, and this means that one can often prove combinatorial properties of these sequences "automatically", using the free software Walnut written by Hamoon Mousavi. In this talk I will explain how this is done, using as an example the measure of minimize size string attractor, introduced by Kempa and Prezza in 2018.
Using the logic-based approach, we can also prove more general properties of string attractors for automatic sequences. This is joint work with Luke Schaeffer.
BibTeX - Entry
@InProceedings{shallit:LIPIcs.CPM.2022.2,
author = {Shallit, Jeffrey},
title = {{Using Automata and a Decision Procedure to Prove Results in Pattern Matching}},
booktitle = {33rd Annual Symposium on Combinatorial Pattern Matching (CPM 2022)},
pages = {2:1--2:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-234-1},
ISSN = {1868-8969},
year = {2022},
volume = {223},
editor = {Bannai, Hideo and Holub, Jan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16129},
URN = {urn:nbn:de:0030-drops-161297},
doi = {10.4230/LIPIcs.CPM.2022.2},
annote = {Keywords: finite automata, decision procedure, automatic sequence, Thue-Morse sequence, Fibonacci word, string attractor}
}
|
Keywords: |
|
finite automata, decision procedure, automatic sequence, Thue-Morse sequence, Fibonacci word, string attractor |
|
Collection: |
|
33rd Annual Symposium on Combinatorial Pattern Matching (CPM 2022) |
|
Issue Date: |
|
2022 |
|
Date of publication: |
|
22.06.2022 |
