Rechnergestütztes Beweisen

Software

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 dass 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 (für Emacs) oder pvs -emacs xemacs (für XEmacs).

Spass

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

zChaff

zChaff SAT Solver. Am CIP: Aufruf mit zchaff.

AndreasAbel Last modified: Wed Dec 14 16:53:39 CET 2005