Bachelorarbeit "Interaktiver Beweisassistent für höherstufige Logik"

Saarland University
Computer Science
Programming Systems
People

Bachelorarbeit

Christian Hümbert, Betreuer: Gert Smolka

Download Bereich

Für Windows/Linux/Unix/Mac:

• Beweisassistent NED
  
  

  Komplettpaket Windows:

• NED+ProofGeneral (inkl. XEmacs Package 42MB)
  
  

  Komplettpaket Linux/Unix/Mac:

• NED+ProofGeneral
  
  

  Nützlich:

• ProofGeneral Homepage
  
  
• Moscow ML System

Allgemeines

Laden Sie den Beweisassistenten NED herunter und befolgen Sie die Anweisungen im unteren Abschnitt Installation NED.

Wenn sie NED in Kombination mit dem Werkzeug ProofGeneral verwenden wollen, laden sie das Komplettpaket (NED + ProofGeneral) herunter und installieren dieses gemäss der unten stehenden Anleitung.

Ist in Ihrem System bereits ProofGeneral installiert, so benötigen Sie ausschliesslich NED. Ihre ProofGeneral Installation müssen sie wie unten erklärt anpassen.

Installation NED

Für die Installation des Beweisassistenten NED benötigen sie eine korrekt installierte Moscow ML Umgebung.
Laden Sie den Beweisassistenten NED herunter und beachten Sie folgende Schritte:

• NED.zip - Entpacken Sie das Zip-Archiv. Es wird automatisch ein Verzeichnis NED angelegt.
  
  
• ned.sml - Um NED zu starten, benutzen Sie Ihren ML-Interpreter und laden die Datei ned.sml
  

Installation Komplettpaket NED+ProofGeneral

Für die Installation des Paketes NED+ProofGeneral benötigen sie eine korrekt installierte Moscow ML Umgebung.
Laden Sie das Komplettpaket NED+ProofGeneral herunter und beachten Sie folgende Schritte:

• tar xfz NEDPackLinux.tar.gz (Linux)
  unzip NEDPackWin.zip (Windows) - Entpacken Sie das Archiv in Ihrem HOME-Verzeichnis (!). Es wird automatisch ein Verzeichnis NEDPackage angelegt
  
  
• cd NEDPackage
  ./install (Linux)
  install.bat (Windows) - Übersetzen Sie die Quellcodes
  (Stellen Sie sicher, dass das Programm mosml im Suchpfad gesetzt ist oder ändern sie entsprechend ./NED/src/Makefile ab)
  
  
• ./start (Linux)
  start.bat (Windows) - Startet ProofGeneral
  
  Es empfiehlt sich, ~/NEDPackage/ProofGeneral/bin/ in Ihrem Suchpfad zu setzen. Sie können dann in einem beliebigen Verzeichnis mit proofgeneral example.ned ein Beweisskript example.ned laden.

Bestehende Proof General Installation an NED anpassen

Stellen Sie sicher, dass sie NED korrekt installiert haben. Informationen zur Software ProofGeneral entnehmen Sie bitte deren Homepage.
Um NED innerhalb des Beweistools ProofGeneral nutzen zu können, müssen einige Erweiterungen vorgenommen werden:

• cd ~/NED Wechseln Sie bitte in das Hauptverzeichnis von NED
  
  
• Kopieren Sie nun das gesamte Verzeichnis nedpg in das Hauptverzeichnis von Proof General
  z.B.: cp -r nedpg/ /usr/local/ProofGeneral/
  
  
• Damit der Beweismodus bereits beim Laden eines Beweisskriptes aktiviert wird, fügen sie bitte die Zeile
  (nedpg "NED" "\\.ned$") im Bereich
  Master table of supported proof assistants
  in der Datei
  ProofGeneral/generic/proof-site.el
  hinzu

Christian Hümbert, 2005