*Wissenschaftliches Programm*   *Liste der Vortragenden*

Sektion 14
Montag, 18.09.2000, 15.00–15.20 Uhr, WIL A 317

Der PCS-Beweiser im Rahmen des Theorema-Projekts

Bruno Buchberger, Johannes-Kepler-Universität Linz, Institut RISC

Der PCS-Beweiser (PCS = “Prove, Compute, Solve”) ist ein neuartiger automatischer Beweiser, der vor allem für den Beweis von Sätzen im Bereich der elementaren Analysis und anderen Gebieten gedacht ist, in welchen die typischen Definitionen alternatierende Quantoren verwenden. Solche Definitionen sind zum Beispiel die Definition des Grenzwertes oder die Definition der Stetigkeit. Das Ziel dieses Beweisers ist die automatische Generierung von Beweisen in einem natürlichen, leicht lesbaren Stil mit möglichst viel Information über die im Beweis enthaltenen Konstruktionen.

Der PCS-Beweiser arbeitet in drei alternatierenden Phasen:

Die P-Phase: Anwenden von allgemeinen prädikatenlogischen Regeln unabhängig vom Inhalt der verwendeten Definitionen zur Grobstrukturierung des Beweises.
Die C-Phase: Anwenden von Definitionen und Hilfssätzen im Stile des “symbolischen Rechnens”, d.h. im Stile von Rewrite-Regeln.
Die S-Phase: Beweis der verbleibenden existentiell quantifizierten Zielformeln durch Aufruf spezieller algebraischer Constraint-Solver wie z.B. des Gröbner-Basen-Verfahrens oder des Verfahrens der zylindrisch- algebraischen Dekomposition.
Durch die spezielle Kombination der Methoden werden die meisten Beweise in einem relativ schlanken Suchraum gefunden. Im Vortrag werden die methodischen Details besprochen und auch Live-Demos gegeben.