Deduce: Ein Beweisprüfer für Bildungszwecke
2025-03-24
Deduce ist ein automatisierter Beweisprüfer, der für den Einsatz in der Bildung entwickelt wurde, um Studenten dabei zu helfen, die Korrektheit von funktionalen Programmen zu beweisen, ihr Verständnis von Logik zu vertiefen und ihre Fähigkeiten im Schreiben mathematischer Beweise zu verbessern. Er richtet sich an Studenten mit grundlegenden Programmierkenntnissen (Java, Python oder C++) und einigen Vorkenntnissen in Logik aus einem Kurs in Diskreter Mathematik. Deduce bietet Ressourcen von der Installation und dem Schreiben von Code bis hin zu einem Referenzhandbuch und einem Spickzettel, mit einem Beispielbeweis eines linearen Suchalgorithmus zur Veranschaulichung seiner Verwendung.