Automatic Theorem Proving in Walnut

2016/03/18 by Mousavi, Hamoon · 9 citations
#Combinatorics (math.CO) #FOS: Computer and information sciences #FOS: Mathematics #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Mathematical Software (cs.MS)

paper · doi:10.48550/arxiv.1603.06017

Abstract

Walnut is a software package that implements a mechanical decision procedure for deciding certain combinatorial properties of some special words referred to as automatic words or automatic sequences. Walnut is written in Java and is open source. It is licensed under GNU General Public License.

Cited by

• Variants of Wythoff game with terminal positions or blocking maneuvers
• On a sequence of Kimberling and its relationship to the Tribonacci word
• Group Actions and Some Combinatorics on Words with vtm
• Balanced Fibonacci word rectangles, and beyond
• New properties of the φ-representation of integers
• Self-Verifying Predicates in Büchi Arithmetic
• On Cloitre's hiccup sequences
• Words with factor complexity 2n+1 and minimal critical exponent
• Shifting Zeckendorf and Chung-Graham representations

Related

• Mechanical proving with Walnut for squares and cubes in partial words
• Exploring the Crochemore and Ziv-Lempel factorizations of some automatic sequences with the software Walnut
• Using Walnut to solve problems from the OEIS
• Automatic verification and interactive theorem proving
• Transduction of Automatic Sequences and Applications