Servus,
in Wikipedia bin ich hier (http://de.wikipedia.org/wiki/Vier-Farben-Satz) auf die Erwähnung eines „Beweisassistenten Coq“ gestoßen. (Zweitletzter Abschnitt im Punkt Geschichte). Was ist dieses Coq genau? Ist das eine Software, die beim Beweisen hilft? Kann sowas überhaupt programmiert werden? Ich dachte immer das sein unmöglich. Allerdings wird ja im Text nur erwähnt, dass es ein „System“ ist. Es kann also auch ein „Beweisverfahren“ wie z.B. die vollstädnige Induktion sein.
Gruß,
Timo