Abstract
In this note, we describe how a fragment of arithmetic can be decided in practice. We follow essentially the ideas of [Thatcher & Wright], which we have embedded in the Mona tool.
Mona is an implementation of Monadic Second-order Logic on finite strings (and trees). The previous semantics used in Mona is the one provided in current literature [Straubing, Thomas], where the meaning of first-order terms is restricted to being a position in the string over which the formula is interpreted.
In this note, we describe our new semantics, where terms are interpreted relative to all natural numbers. With this semantics Mona becomes a decision procedure for the calculus called WS1S, the Weak Second-order theory of 1 Successor.
We also show how the Mona representation of automata subsumes a recent proposal for representing queues. We exploit the natural semantics to carry out automated reasoning about queue operations.