Build numbers, step through addition, and evaluate formulas — all from the axioms.
Every natural number is built by applying the successor function S to 0. Click S( ) to wrap another layer.
Watch Presburger addition unfold axiom by axiom. Axiom 4 peels one S from the second argument; Axiom 3 resolves the base case.
Select a Presburger sentence and evaluate it. The decision procedure always terminates with the correct answer.