In der Aussagenlogik gibt es eine Reihe von Gesetzen, mit denen man Beweise führen kann, z.B. den Beweis, dass die Aussage (p (¬q p)) T eine Tautologie ist, also immer T. Das Programm gibt das Gesetz an, das Sie auf die jeweilige Ausgangsformel anwenden sollen. Daraus ergibt sich ein neuer Ausdruck, der mit Hilfe der Bildertastatur auf die Zeile "Gesuchte Zielformel" geschrieben werden kann. Mit "Löschen" kann man rücklöschen, wenn man einen Fehler gemacht hat. Wenn man fertig ist, klickt man auf "Prüfen". Die Eingabe wird korrigiert, und das Programm gibt das nächste anzuwendende Gesetz an.