Rechnergestütztes Beweisen

Software

Eine abhängig getypte Programmiersprache ähnlich Haskell. Experimentell, am CIP nicht installiert.

Coq IDE

Eine eigene graphische Benutzeroberfläuche, coqide, ist auf lichtenberg.cip.ifi.lmu.de installiert, als Alternative zu emacs/proofgeneral. Aufruf:

ssh -X lichtenberg.cip.ifi.lmu.de
coqide

Coq

Coq, ein konstruktives interaktives Beweissystem. Dazu den emacs-Mode Proof General.

Coq ist (dank Thomas Bleher) am CIP installiert, zusammen mit dem Emacs-Interface ProofGeneral. Um ProofGeneral zu aktivieren, bitte in der Datei .emacs (ist für XEmacs manchmal .xemacs/init.el) die Zeile

(load-file "/soft/IFI/text/emacs-21.2/iX86-unknown-linux/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")

hinzufügen. Da im CIP üblicherweise UTF-8 angeschalten ist, aber ProofGeneral mit der UTF-8 Konvertierung Probleme hat (siehe die FAQ), muss man UTF im Locale abschalten, bevor man den (X)Emacs startet. In der CShell erreicht man das z.B. mit

setenv LC_CTYPE de_DE; emacs &

in der bash mit

LC_CTYPE=de_DE emacs &

ProofGeneral wird gestartet, sobald man eine Datei mit der Endung .v öffnet.

PVS

Prototype Verification System. Ist am CIP installiert. Aufruf:

pvs

am Besten bereits vom richtigen Verzeichnis aus (ansonsten mit M-x change-context in PVS das Verzeichnis wechseln). Achtung! Sofortiges Laden einer Datei mit pvs datei.pvs bringt pvs durcheinander! Daher pvs immer leer starten.

Die Emacs-Variante kann man auswählen, z.B. pvs -emacs emacs21. Allerdings werden wohl nicht alle Emacs-Varianten unterstützt.

Alte Instruktion (2007-11-12): Im Moment fehlt an einigen CIP Rechnern der Pfad auf pvs. Aufruf mit:

/soft/IFI/sci/PVS-4.0/iX86-unknown-linux/pvs -emacs emacs21

Spass

SPASS, ein automatischer Beweiser für Logik erster Stufe. Am CIP: Aufruf mit SPASS. Eingabesyntax.

Tutch

Tutch (Tutorial proof checker). Beweisprüfer für konstruktives natürliches Schließen. Zu Übungszwecken.
Installation am CIP:

tutch-0.52-for-sml-110.45.tar.gz herunterladen und auspacken. In das ausgepacke Verzeichnis wechseln.

wget http://www.tcs.ifi.lmu.de/~abel/tutch/tutch-0.52-for-sml-110.45.tar.gz
tar xzf tutch-0.52-for-sml-110.45.tar.gz
cd tutch-0.52

Die Umgebungs-Variable SMLNJ_HOME setzen. In der CShell erreicht man das mit
```
setenv SMLNJ_HOME /soft/IFI/lang/smlnj-110.65/iX86-unknown-linux/
```
in der bash mit
```
export SMLNJ_HOME=/soft/IFI/lang/smlnj-110.65/iX86-unknown-linux/
```
(Tipp: Mit echo $SHELL kann man testen, welche Shell man fährt.)
Dieser Schritt ist im Moment (2007-10-31) erforderlich, aber in Zukunft nicht mehr nötig, wenn die SML Installation am CIP wieder stabil ist.
Tutch compilieren mit
```
make
```
Dies erzeugt im Unterverzeichnis bin ein Shell-Skript tutch.
Tutch testen mit
```
bin/tutch
```

zChaff

zChaff SAT Solver. Am CIP: Aufruf mit zchaff.

AndreasAbel

Last modified: Fri Nov 16 21:58:26 CET 2007