Maschinengestütztes Beweisen

Maschinengestütztes Beweisen (oder missverständlicher: automatisches Beweisen; ein Teilgebiet der automatischen Deduktion) basiert auf der Verwendung von Computerprogrammen zur Erzeugung und Überprüfung von mathematischen Beweisen logischer Theoreme. Im Unterschied zu einem Computerbeweis wird versucht, den gesamten formalen Beweis bestehend aus Schritten und Zwischenergebnissen zu konstruieren.

  1. ↑ Vgl. Übersichtsartikel von T. Hales (2008), Formal Proof (PDF; 524 kB).
Dieser Artikel wurde von Wikipedia herausgegeben. Der Text ist unter Creative Commons Attribution-Share Alike 4.0 verfügbar, sofern nicht anders angegeben. Für die Mediendateien können zusätzliche Bedingungen gelten.