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
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.; Petermann, U.; Bibel, W. et al.
- Chapter II.6: Theory Reasoning
- Baumgartner, P.
- Theory Reasoning in Connection Calculi
- Baumgartner, Peter; Furbach, Ulrich
- Variants of Clausal Tableaux
- 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, Peter; Furbach, Ulrich; Stolzenburg, Frieder
- 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
