26.6.: H. Ganzinger, Integration von Entscheidungsverfahren in

From: Helmut Veith (kgs-owner@dbai.tuwien.ac.at)
Date: Mon Jun 24 2002 - 12:21:01 MEST

  • Next message: Helmut Veith: "July 2: T. Forstner, Set Theories with a Universal Set"

    Lecture Announcement
    =====================

    Integration von Entscheidungsverfahren in Beweiser f"ur Logik erster Stufe
    --------------------------------------------------------------------------
    Harald Ganzinger, Max-Planck-Institut fuer Informatik, Saarbr"ucken

    ABSTRACT: Viele Anwendungen f"ur automatisches Beweisen brauchen sowohl
    konkrete mathematische Theorien, wie Zahlen, Listen, arrays, als auch
    abstrakt definierte Strukturen der jeweiligen Dom"ane. Gute Beweiser
    m"ussen daher die klassischen Techniken des Rechnens und Beweisens f"ur
    Standardstrukturen mit den Inferenzsystemen aus der universellen Algebra
    und Logik kombinieren. Der Vortrag bespricht wesentliche Konzepte einer
    solchen Kombination, insbesondere die Verfahren nach Nelson/Oppen  und
    Shostak, sowie Ans"atze zu Theorieresolution und -Superposition.

    TIME: Wednesday, June 26, 14.00
    PLACE: Seminarraum 185/2, Favoritenstrasse 9, Stiege 1, 3. Stock, TU
    Vienna



    This archive was generated by hypermail 2b30 : Mon Jun 24 2002 - 12:22:28 MEST