Hauptseminar "Beweissysteme" (WS 96/97)

Inhaltsverzeichnis dieser Seite

Organisatorisches

Hauptseminar:

Beweissysteme. 3

Betreuer: Slim Abdennadher, Norbert Eisinger, Tim Geisler, Sunna Torge

Zeit und Ort: Di 13-15 Uhr, Raum 033; Di 15-16 Uhr, Raum Z106, Oettingenstr. 67

Beginn: 5.11.1996

Themenvergabe:

in der ersten Sitzung am Di 5.11.1996 oder vorher bei den Betreuern

für:

Haupt- und Nebenfach Informatik

Vorkenntnisse:

Grundkenntnisse von Deduktionssystemen

Schein:

Gilt für Diplomprüfung Haupt- und Nebenfach Informatik

Inhalt des Seminars

Im Seminar werden implementierte und verfügbare automatische Beweissysteme vorgestellt und vorgeführt. Der Schwerpunkt liegt auf Widerlegungssystemen und Modellgenerierungssystemen für die klassische Prädikatenlogik erster Stufe. Aber auch andere Arten von Beweissystemen (zum Beispiel Induktionsbeweiser, Gleichheitsbeweiser, Beweiser für andere Logiken) können je nach Interesse behandelt werden.

Die Seminarteilnehmer sollen im Vortrag die formalen Grundlagen des jeweiligen Systems vorstellen. Anstelle einer schriftlichen Ausarbeitung soll das System auf den CIP-Rechnern installiert und mit zugehörigen Beispielen vorgeführt werden.

Vorträge

Klassische Widerlegungsbeweiser

Otter

ist der klassische auf Resolution und Paramodulation basierende Beweiser für die Prädikatenlogik erster Stufe mit Gleichheit.

W. McCune (Argonne National Laboratories)

http://www.mcs.anl.gov/home/mccune/ar/otter/

Setheo

ist ein auf Konnektionstableaux basierender Beweiser für die Prädikatenlogik erster Stufe.

Automated Reasoning Group (TU München)

http://wwwjessen.informatik.tu-muenchen.de/forschung/reasoning/setheo.html

CLIN

ist ein Widerlegungsbeweiser für Klausellogik. Vorgehensweise in zwei Phasen: Erzeugung von Grundinstanzen, Widerlegung nach "Clause-Linking" Methode.

D. Plaisted (U North Carolina), G. Alexander (IBM)

http://www.cs.unc.edu/Research/mi/mi-provers.html

LeanTAP

ist ein in einigen Zeilen Prolog implementierter Tableaubeweiser für die Prädikatenlogik erster Stufe.

B. Beckert, J. Posegga (Uni Karlsruhe)

http://i12www.ira.uka.de/~posegga/leantap/leantap.html

3TAP

ist ein auf Tableaux basierender Beweiser für beliebige endlich-wertige Logiken erster Stufe. Gleichheit, Sorten und Nicht-Klauselform können behandelt werden.

B. Beckert (Uni Karlsruhe)

http://i12www.ira.uka.de/~threetap/

PROTEIN

ist ein automatischer Beweiser für Klausellogik auf der Grundlage der Modellelimination.

P. Baumgartner, U. Furbach (Uni Koblenz)

http://www.uni-koblenz.de/ag-ki/Systems/PROTEIN/

Saturate

basiert auf dem Superpositionskalkül (Variante der Termersetzung). Besondere Methoden zur Behandlung transitiver Relationen.

H. Ganzinger, R. Nieuwenhuis (MPI Saarbrücken)

http://www.mpi-sb.mpg.de/SATURATE

SPASS

basiert auf dem Superpositionskalkül erweitert um Sorten.

C. Weidenbach (MPI Saarbrücken)

http://www.mpi-sb.mpg.de/guide/software/spass.html

Modellgeneratoren

MACE

ist ein System zur Berechnung kleiner endlicher Modelle für die Prädikatenlogik erster Stufe und basiert auf dem Davis-Putnam-Verfahren.

W. McCune (Argonne National Laboratories)

http://www.mcs.anl.gov/home/mccune/ar/mace

FINDER

(Finite Domain Enumerator) berechnet mittels exhaustiver Suche Modelle einer gegebenen Kardinalität, wobei die gegebene Klauselmenge als Constraints verwendet werden.

John Slaney (Australian National University)

http://arp.anu.edu.au/arp/jks/finder.html

SEM

(System for Enumerating Models) ist ein weiteres System zur Berechnung von Modellen einer gegebenen Kardinalität.

Jian Zhang, Hantao Zhang (Univ. of Iowa)

file://cs.uiowa.edu/pub/hzhang/sem

Beweissysteme für nichtklassische Logiken

Logics Workbench (LWB)

ist ein interaktiver Beweiser für klassische und nicht-klassische Aussagenlogiken.

G. Jäger, A. Heuerding, S. Schwendimann (Uni Bern)

http://lwbwww.unibe.ch:8080/cgi-bin/LWBinfo?request=home

ACL2

ist ein automatischer/interaktiver Beweiser für eine rein funktionale Teilsprache von Common Lisp und wird komerziell für große Verifikationsanwendungen eingesetzt.

Matt Kaufmann, J. Strother Moore (Computational Logic Inc.)

http://www.cli.com/software/acl2/index.html

Isabelle

ist ein generischer Beweiser, in dem die verwendeten Logiken und Beweistaktiken spezifiziert werden können.

Lawrence C. Paulson (Cambridge), Tobias Nipkow (TU München)

http://www.cl.cam.ac.uk/Research/HVG/isabelle.html

Teilnehmerliste

Lehr- und Forschungseinheit

Institut

Universität