In diesem Bereich sind eine Reihe unterschiedlicher Aktivitäten zusammengefaßt, die auf Logik als Beschreibungssprache sowie der Verarbeitung dieser Beschreibung basieren. Der zentrale Bergriff ist hierbei die Deduktion, also das Bilden und Überprüfen von Schlußfolgerungen und hierfür geeignete Verfahren. Solche Verfahren finden ihre Anwendung auch in Teilprojekten, die sich mit Theorembeweisern, deduktiven Datenbanken und der Verifikation von parallelen logischen Programmen befassen.
Ein wichtiger Aspekt hierbei ist die Beurteilung der Leistungsfähigkeit von verschiedenen Beweisverfahren. Hier interessiert sowohl die Fragestellung, welche Verfahren für welche Aufgaben am besten geeignet sind, als auch der Vergleich verschiedener Beweiskalküle. Neben empirischen Untersuchungen des Laufzeitverhaltens konkreter deterministischer Inferenzalgorithmen im Worst-Case und im Average-case ist man hier besonders an exakten theoretisch fundierten Aussagen interessiert, wie sie schon exemplarisch für aussagenlogische Beweisverfahren angegeben werden konnten.
Weitere Teilprojekte befassen sich mit der effizienten Implementierung von Logikverfahren, sowie der Entwicklung von Herleitungsstrategien und exemplarischen Theorembeweisern, die die Vorteile unterschiedlicher Verfahren nutzen. Ein Schwerpunkt liegt hierbei auch auf der Untersuchung von parallelen Theorembeweisern.
Abgerundet werden die Untersuchungen von Teilprojekten. die sich mit logikbasierter Wissensrepräsentation und der Entwicklung entsprechender Beweiskalküle befassen. Hierbei sind insbesondere nicht-klassische Logiken, Konzepte des nicht-monotonen Schließens und ihre Beziehung zur logischen Programmierung von Interesse.
Projektpartner:
Kontakt:
Prof. Dr. H. Kleine Büning Universität-GH Paderborn Warburgstraße 100, 33095 Paderborn Tel.: (05251) 60-3361 email: kbcsl@uni-paderborn.de
KI-NRW