Was ist MONA?
Übersetzt von der Website des Projekts: "MONA implementiert Entscheidungsverfahren für Weak Second-order Theory of One or Two successors (WS1S/WS2S). Die Theorie eines Nachfolgers, bekannt als WS1S, ist ein Fragment der Arithmetik, ergänzt durch Quantifizierung zweiter Ordnung über endliche Mengen natürlicher Zahlen. Seine Terme erster Ordnung bezeichnen nur natürliche Zahlen. Die Theorie hat keine Addition, da sie dadurch unentscheidbar wäre, aber sie verfügt über eine unäre Operation +1, die sogenannte Nachfolgefunktion. WS2S ist eine Verallgemeinerung auf Baumstrukturen."