Rechnergestütztes Beweisen

Software

Agda
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:
  1. 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
    
  2. 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.
  3. Tutch compilieren mit
    make
    
    Dies erzeugt im Unterverzeichnis bin ein Shell-Skript tutch.
  4. Tutch testen mit
    bin/tutch
    
zChaff
zChaff SAT Solver. Am CIP: Aufruf mit zchaff.


Valid HTML 4.01!
AndreasAbel
Last modified: Fri Nov 16 21:58:26 CET 2007
Valid CSS!