Pith. Sign in

REVIEW

Automatic Theorem Proving in Walnut

PaperPDF from arXiv

data files

ReviewThe objections and verdict, as JSON Paper breakdownThe authors' claims, conditions and measurements, as JSON Signed receiptProof this review has not been altered
X Bluesky LinkedIn Reddit Hacker News
Hamoon Mousavi

Formal Languages and Automata Theory · Submitted 18 Mar 2016 · 15 references

Pith's verdict: The Walnut manual: a solid, honest tool reference whose one undelimited caveat in §4.2 is a documentation gap, not a flaw in the underlying procedure.

T0 · AI review

How this review was made: An AI referee (selfhosted/deepseek-v4.1-flash) read the paper on October 29, 2026 and answered a fixed list of questions about it. T0 is the starting level every paper gets. The levels describe how deeply Pith has checked the paper, never the authors.

  1. T0 AI review An AI read the paper and answered a fixed list of questions.
  2. T1 Audit Automatic checks that the references and files the paper relies on exist and match.
  3. T2 Compute The paper's code or calculations re-run with the same results.
  4. T3 Formal statement The claims written out in a formal math language a computer can read.
  5. T4 Proof Those claims proved, and the proof checked by computer.

How Pith checks papers →

· 2 major objections · 7 minor · Ask about this paper · The compiled record · Read the full review →
Challenge this review Comment (0) Read on arXiv ↗
Cite ▾
arXiv ID1603.06017 (version 2)
Pith IDOBHPWXJH, Pith's permanent record of this paper and its review
CitationHamoon Mousavi. "Automatic Theorem Proving in Walnut." arXiv:1603.06017 (2016). https://pith.science/paper/OBHPWXJH
Cite this reviewBibTeX for Pith's review of this paper
Claim paper

Why Pith says this

Highlight any text to comment on it.

Referee report

How Pith checks papers → · Full audit of this paper →

The paper

The paper claims

Walnut turns questions about automatic words into finite automata, so a predicate about a sequence is decided by a machine rather than by finding a proof.

The reading

Walnut is a program that answers questions about automatic words: infinite sequences, such as the Thue–Morse word, whose $n$-th symbol is produced by a finite automaton reading a representation of $n$. The claim the article sets out to establish is that a user can write a property of such a word in a formal predicate language, submit it, and receive back a finite automaton that accepts exactly the tuples of positions satisfying that property; the property holds somewhere if and only if the automaton accepts at least one word, and holds nowhere if it accepts none. That matters because it converts a class of combinatorial questions — does this word contain a square of every order, does it avoid overlaps, which lengths actually occur — into a terminating computation whose answer can be drawn and inspected. The article is written as a guide rather than a proof paper: it fixes notation for number systems and automatic words, defines the predicate syntax and its semantics, walks through the automaton construction that implements each logical, arithmetic, calling, and indexing operator, and then documents the commands, file formats, and worked examples. Two of those examples carry the point: the orders of squares in the Thue–Morse word come out as the set of $n$ of the form $2^k$ or $2^{k+1}+2^k$, and the check that the Thue–Morse word avoids overlaps returns the one-state true automaton.

What carries the argument

The load-bearing mechanism is the cross product of automata, which builds the machine for a conjunction from the machines for its two halves by running them in parallel and keeping only pairs of accepting states, with analogous choices of final-state set giving disjunction, exclusive or, implication, and equivalence. Quantification is handled by projection: the quantified coordinate is deleted from every transition, producing a nondeterministic automaton that misses exactly those tuples whose witness exists only after padding with leading or trailing zeros, and the paper's repair is to seed the start states (for most-significant-digit systems) or the final states (for least-significant-digit systems) with everything reachable by reading a string of zeros, then determinize and minimize. Negation is totalization plus swapping final and non-final states, intersected with the automaton for valid representations so that non-representations are not accidentally accepted. Arithmetic and comparison operators are then built recursively from addition and less-than, indexing into a word is read off the final states of that word's automaton with output, and calling a named automaton is shown to be pure syntactic sugar over an existential quantification plus equalities.

Extended reading notes

Core claim

The central claim is that the first-order theory of the natural numbers, extended with the ability to index into automatic words, is decidable in practice, and that Walnut is an implementation of that decision procedure. Every predicate in the language is built from four base relations that each number system supplies — valid representations, addition, equality, and less-than — together with the logical connectives, quantifiers, arithmetic operators, calls to previously defined automata, and indexing expressions. The paper's assertion is that for every such predicate and every ordering of its free variables there is a unique minimal deterministic automaton accepting exactly the same-length representations of the tuples that satisfy it, and that this automaton can be computed by cross product, projection, complementation, and minimization. The author states the consequence directly: questions about squares, overlaps, palindromes, borders, and factor complexity in an automatic word become computations, and the output is not merely a yes or no but a machine describing the entire set of satisfying tuples.

Load-bearing premise

The load-bearing premise is that the automaton built for an existential quantifier accepts exactly the tuples that have a witness; the paper states this holds only when the surviving inputs are all most-significant-digit-first or all least-significant-digit-first, and says that for mixed systems the program builds only the raw projection, which the author calls not theoretically accurate and asks users to be cautious about.

Editorial extensions

If this is right

  • Every property expressible in the predicate language is decidable, so questions about squares, overlaps, palindromes, borders, and factor complexity in an automatic word become computations rather than proof searches.
  • Because the result is a minimal automaton rather than a bare yes or no, the answer describes the whole set of satisfying tuples, as with the square orders in the Thue–Morse word emerging as $2^k$ and $2^{k+1}+2^k$.
  • Predicates can be named with `def` and called from later predicates, so a reusable library of lemmas about a word can be accumulated and cited inside subsequent queries.
  • Asking for incidence matrices of chosen free variables lets a user count or enumerate solutions instead of merely deciding existence.
  • Regular-expression input through `reg` lets a user hand-build automata for sets that Presburger arithmetic cannot express, such as the powers of two, and mix them into later predicates.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The practical reach of the tool is set less by the logic than by which sequences someone has already encoded as automata with output, so the interesting near-term work is expanding that library rather than expanding the predicate language.
  • The acknowledged gap for mixed most-significant-digit and least-significant-digit quantification suggests a concrete repair: carry the padding length as an extra existentially quantified coordinate, which would make the projection exact in the mixed case instead of merely approximate.
  • Since the output is an automaton rather than a proof script, an answer can be checked by a small trusted automaton library, which is a much weaker trust requirement than trusting a general-purpose theorem prover.
  • The predicate language behaves like a programming language with quantifiers, so the cost of a query is dominated by determinization and minimization; the practical barrier is state blow-up, not the difficulty of the underlying logic.
Original 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.

The compiled record

The paper's own sentences, arranged, kept beside the review and separate from it. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.

Compiled by classifier-1.13.0 via TypeSafe API, question bank abstract-p1-20260923, 2026-09-23: 1 request, 2,806 input tokens.

What the abstract itself states, as probabilities: claims first 0.03 · states limitation 0.20 · human participants 0.02 · controlled comparison 0.01 · randomized assignment 0.01 · states quantitative result 0.03 · compares with prior results 0.03 · mentions code or data availability 0.85.

The abstract, sentence by sentence

arXiv listing abstract v2. Results and the main claim are underlined; .

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.

background contribution method result interpretation main claim

What the classifier reports for each sentence. The number is the probability it gave the label.
#sentencerolethe authors' own workstates the main conclusionstrength
s0 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. contribution 0.49 0.33 0.19 asserted 1.00
s1 Walnut is written in Java and is open source. method 0.68 0.47 0.03 asserted 1.00
s2 It is licensed under GNU General Public License. background 0.88 0.22 0.02 asserted 1.00

What kind of paper the classifier reports this is: method or tool 1.00 · evidence from simulation or computation 0.49.

What was examined, and what was not

sources read
  • arXiv listing abstract v2
not examined
  • full text
  • figures and tables
  • references and citing sentences
  • relations to other papers
levels run
  • P abstract
not run
  • S sections
  • T body sentences
  • C citations
  • R cross-paper relations

Every quoted sentence on this record is the authors'. Every label is from Pith's closed vocabulary, with the probability shown beside it. Every number in the measurements table is the authors', checked by code. Record as JSON

Figures
Figure 2. 6: Automaton computing Rmsd_fib In cases, where an automaton’s inputs are representations of integers in some number system, which by far are the most important type of automata in Walnut, we would like to signify these number systems instead of the input alphabets. For example, we might write ¡ Q,q0,F,δ,S1,S2,...,Sn ¢ to mean ¡ Q,q0,F,δ,ΣS1 ,ΣS2 ,...,ΣSn ¢ . It should be understood that in these cases, if for a word w input πj(w) is not a valid representation in Sj , it does not mean that the automaton’s behavior is not defined for w. This just means that w is, by default, not going…
Figure 4. 7: (a) : Eb a = 1 &b = 2 Currently if for (x1,...,xn) : P it is not the case that for all j 6= i number systems Sj are all msd or all lsd, then Walnut only constructs E(M,i) for Exi P, which is not theoretically accurate. So the user has to be very cautious when quantifying predicates over mixed msd and lsd number systems, or in cases where the quantified automaton is non-arithmetic. For a definition of the latter see Section 5.2. To obtain an automaton for AxiP, note its equivalence to ∼ (Exi ∼ (P)), where ∼ is the logical complement (negation). See the next section to learn about…
Figure 5. 2: False automaton
Figure 7. 10: another_nonsense.gv The number of arguments when calling an automaton should match the number of inputs of that automaton: eval in v alid "$sum10(x, y, z)" ; function sum10 requires 2 arguments : char a t 1 : eval in v alid "$sum10(x, y, z)" ; Always remember the roles of the inputs to an automaton created by the def command. For example, look at the following examples of the def command: def f1 "y < x" ; def f2 "x < y " ; Now the following evaluates to an automaton accepting representations of numbers > 1: eval greater_than_1 " $ f1 (a , 1 ) " ; whereas the following evaluates to
Figure 8. 1: Automata for paperfolding words This automaton is defined in the file PF.txt in directory “/Walnut/Word Automata Library/”: 14If an automaton does not follow these criteria we can always come up with an isomorphic one that does. 15File names in Walnut start with letters and can contain alphanumerics and underscore. 32

Showing 5 of the paper's 8 figures. See all figures in the PDF ↗ Figures reproduced from arXiv:1603.06017 by the authors.

References
How later papers used it

93 later papers cite it

Evidence: substantial. 93 of the citing papers share no author with it, and 81 of those carry a confident label from Pith's citation classifier.

Pith read 25 of the 111 citing sentences, choosing only those whose citation markers point at this paper alone, and wrote the paraphrases from them. The summary, the counts, the evidence level, the links and the quotes come from code; the summary counts the papers listed below. A later paper is listed under a label when Pith's citation classifier gives one of its sentences that label at probability 0.8 or more (0.95 for support), Pith's reading finds that the citing paper itself did it, and a second check confirms the paraphrase against the sentence. This section lists uses only. It does not list criticism or disagreement, so their absence here says nothing about how the paper has been received. Papers that share an author with this one are listed apart, under "By the same authors". A quote is the citing authors' own sentence, shown when their paper's licence is CC BY, CC BY-SA or CC0. JSON

Uses its method or tool 14 of 79 papers with this label
How the literature uses it

90 arXiv papers cite this in 108 sentences

Each citing sentence is taken from the citing paper's LaTeX source and typed by Pith's classifier. A label appears at probability 0.8 or more (0.95 for support), a contest at 0.7 or more; the quoted words are the citing authors'. How each label was checked · JSON

Papers citing it · 17 sentences without a confident label

Uses its method or tool 77 papers
Compares with it 1 paper
Cites it as background 3 papers

Discussion

Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.