GPN16:The Incredible Proof Machine: Unterschied zwischen den Versionen
aus dem Wiki des Entropia e.V., CCC Karlsruhe
(Fahrplanbot tut Dinge) |
K (Fahrplanbot tut Dinge) |
||
| Zeile 1: | Zeile 1: | ||
{{#css: | {{#css:GPN16:Stylesheet}} | ||
Ein Vortrag von Joachim Breitner auf der [[ | Ein Vortrag von Joachim Breitner auf der [[GPN16]]. | ||
Beweise machen Spaß – vor allem mit einem interaktiven Theorembeweiser. Aber während die „großen“ Theorembeweiser wie Isabelle und Coq eine ziemlich hohe Einstiegshürde haben, kann man mit der <i>Incredible Proof Machine</i> direkt loslegen, denn hier bestehen Beweise aus Bausteinen, die man nur richtig verdrahten muss. So wird Beweisen so einfach, aber auch so fesselnd, wie ein gutes Puzzlespiel. | Beweise machen Spaß – vor allem mit einem interaktiven Theorembeweiser. Aber während die „großen“ Theorembeweiser wie Isabelle und Coq eine ziemlich hohe Einstiegshürde haben, kann man mit der <i>Incredible Proof Machine</i> direkt loslegen, denn hier bestehen Beweise aus Bausteinen, die man nur richtig verdrahten muss. So wird Beweisen so einfach, aber auch so fesselnd, wie ein gutes Puzzlespiel. | ||
| Zeile 12: | Zeile 12: | ||
{{Navigationsleiste | {{Navigationsleiste GPN16}} | ||
[[Kategorie: | [[Kategorie:GPN16:Events]] | ||
Version vom 19. Mai 2016, 16:26 Uhr
Ein Vortrag von Joachim Breitner auf der GPN16.
Beweise machen Spaß – vor allem mit einem interaktiven Theorembeweiser. Aber während die „großen“ Theorembeweiser wie Isabelle und Coq eine ziemlich hohe Einstiegshürde haben, kann man mit der Incredible Proof Machine direkt loslegen, denn hier bestehen Beweise aus Bausteinen, die man nur richtig verdrahten muss. So wird Beweisen so einfach, aber auch so fesselnd, wie ein gutes Puzzlespiel.
Im Workshop werde ich euch die Bedienung der Proof Machine als auch ein wenig die theoretischen Hintergründe erklären.
Links