Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Automatic Theorem Proving in Walnut

Hamoon Mousavi

TL;DR

Walnut presents a practical, automata-based framework for deciding properties of automatic words by extending Presburger arithmetic with indexing into automatic words. It provides a comprehensive implementation of a decision procedure built from automata cross products, quantification, and complement/reverse operations, enabling predicates over number-system representations and automatic-word indices. The system supports defining and reusing automata via eval/def/macros, regular-expression automata, and non-arithmetic automata, with compatible I/O tooling and visualization through Graphviz. The approach is demonstrated on classical automatic-word objects like Thue–Morse and Fibonacci words, and the paper also discusses installation, usage, and limitations when handling mixed number systems and non-arithmetic constructs.

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.

Automatic Theorem Proving in Walnut

TL;DR

Walnut presents a practical, automata-based framework for deciding properties of automatic words by extending Presburger arithmetic with indexing into automatic words. It provides a comprehensive implementation of a decision procedure built from automata cross products, quantification, and complement/reverse operations, enabling predicates over number-system representations and automatic-word indices. The system supports defining and reusing automata via eval/def/macros, regular-expression automata, and non-arithmetic automata, with compatible I/O tooling and visualization through Graphviz. The approach is demonstrated on classical automatic-word objects like Thue–Morse and Fibonacci words, and the paper also discusses installation, usage, and limitations when handling mixed number systems and non-arithmetic constructs.

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.

Paper Structure

This paper contains 40 sections, 2 theorems, 34 equations, 44 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Basics
  3. Words and Automata
  4. Number Systems
  5. Automatic Words
  6. Automata accepting Predicates
  7. Syntax and Semantic of Predicates in Walnut
  8. Alphabets
  9. Arithmetic and Alphabetic Constants
  10. Variables
  11. Operators
  12. Arithmetic Expressions
  13. Indexing Expressions and Their Semantic Rules
  14. Calling Expressions and Their Semantic Rules
  15. Relative Expressions
  16. ...and 25 more sections

Key Result

Theorem 6

For $F" = \{(q,q'):q\in F \text{ and } q'\in F'\}$, the automaton $(M\times M')(F")$ accepts predicate $P\mathbin{\&}P'$. Furthermore, minimizing $(M\times M')(F")$, we obtain automaton $(x"_1,\ldots,x"_p):P\mathbin{\&}P'$.

Figures (44)

  • Figure 2.1: Automaton accepting tuples of same length representations of $4$ and $5$ in binary
  • Figure 2.2: Automaton computing $R_{ \bf{msd} }$
  • Figure 2.3: Automaton computing $+_{ \bf{msd} }$
  • Figure 2.4: Automaton computing $=_{ \bf{msd} }$
  • Figure 2.5: Automaton computing $<_{ \bf{msd} }$
  • ...and 39 more figures

Theorems & Definitions (9)

  • Definition 1: relations computed by automata
  • Definition 2: number systems
  • Definition 3: number systems in Walnut
  • Definition 4: semantic rule regarding indexing
  • Definition 5: semantic rule regarding calling
  • Theorem 6
  • proof
  • Lemma 1
  • proof