Theoriebehandlung in Beweisprozeduren für Prädikatenlogik 1. Stufe (TheTP) | SciPort RLP

Durch die Nutzung unserer Webseite erklären Sie sich damit einverstanden, dass wir Cookies verwenden. Weitere Informationen

Theoriebehandlung in Beweisprozeduren für Prädikatenlogik 1. Stufe (TheTP)

Laufzeit: 01.07.1993 - 31.12.1999

Partner: TU München, Gruppe Intellektik; Uni Karlsruhe, Fakultät Informatik, Prof. P. Schmitt

Förderung durch: DFG: Schwerpunktprogramm Deduktion

Kurzfassung

In diesem Projekt betreiben wir Grundlagenforschung auf dem Gebiet des automatischen Theorembeweisens, mit einem Schwerpunkt auf Methoden des Theorieschließens, gewissen Aspekten der Logikprogrammierung und der Modellberechnung. Die theoretischen Arbeiten über den Entwurf von Kalkülen werden durch Systementwicklungen und potentielle praktische Anwendungen komplementiert (Programmverifikation, Modellbasierte Diagnose, Updates in Deduktiven Datenbanken, Wissensmanagement im...In diesem Projekt betreiben wir Grundlagenforschung auf dem Gebiet des automatischen Theorembeweisens, mit einem Schwerpunkt auf Methoden des Theorieschließens, gewissen Aspekten der Logikprogrammierung und der Modellberechnung. Die theoretischen Arbeiten über den Entwurf von Kalkülen werden durch Systementwicklungen und potentielle praktische Anwendungen komplementiert (Programmverifikation, Modellbasierte Diagnose, Updates in Deduktiven Datenbanken, Wissensmanagement im Slicing-Book-Technologie Projekt). Weitere Info im WWW: http://www.uni-koblenz.de/ag-ki/TheTP/» weiterlesen » einklappen

Beweissystems Klauselmengen Konzeptsprachen Gleichheit Modelleliminationskalküle PTTP-Implementierung PROTEIN-System Saturierungsmethoden räumlichen Schließen Kalkülverbesserungen

Veröffentlichungen

Stolzenburg, Frieder
An Algorithm for General Set Unification and Its Complexity

Stolzenburg, F.; Hähnle, H.; Menzel, W. et al.
Loop-Detection in Hyper-Tableaux by Powerful Model Generation

Stolzenburg, Frieder
A flexible System for Constraint Disjunctive Logic Programming

Baumgartner, P.; Furbach, U.; Bibel, W. et al.
Chapter I.3: Variants of Clausal Tableaux

Baumgartner, P.; Petermann, U.; Bibel, W. et al.
Chapter II.6: Theory Reasoning

Baumgartner, P.
Theory Reasoning in Connection Calculi

Baumgartner, Peter; Aravindan, C.; Baumgartner, P. et al.
A Rational and Efficient Algorithm for View Deletion in Databases

Baumgartner, P.; Furbach, U.; J. Maluszynski, J. Maluszynski
Calculi for Disjunctive Logic Programming

Baumgartner, P.; Furbach, U.; Stolzenburg, F.
Computing answers with model elimination

Baumgartner, Peter; P. Baumgartner, P.; Furbach, U.
Refinements for Restart Model Elimination

Baumgartner, P.; Beckert, Bernhard; Kühn, Michael et al.
Extending Hyper Tableaux with Rigid E-Unification

Baumgartner, P.; Furbach, U.; Niemelä, Ilkka
Hyper Tableaux

Furbach, U.; Baumgartner, Peter
Hyper Tableaux and Disjunctive Logic Programming

Baumgartner, Peter
Linear and Unit-Resulting Refutations for Horn Theories

Baumgartner, Peter; Brüning, Stefan
A disjunctive positive refinement of model elimination and its application to subsumption deletion

Stolzenburg, Frieder; Thomas, Bernd
Analysing rule sets for the calculation of banking fees by a theorem prover with constraints

Stolzenburg, Frieder
Membership-constraints and complexity in logic programming with sets

Projektteam

Ulrich Furbach
Mitarbeiter/in
(Institut für Informatik)

Beteiligte Einrichtungen

Künstliche Intelligenz
(Universität Koblenz)