Gleichheitsbeweisen höherer Stufe

• Antragsteller: Professor Dr. Jörg H. Siekmann
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 1996 bis 2003
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5261974

Im Projekt Hotel sollen Verfahren zur Gleichheitsbehandlung für eine Logik höherer Stufe untersucht werden. Dabei sollen grundlegende Techniken zur Mechanisierung der Gleichheit, wie sie aus der Logik erster Stufe bekannt sind, so verallgemeinert werden, daß sie für getypte l-Kalküle einsetzbar werden. Diese Verfahren sollen dann im automatischen Beweisen höherer Stufe (wie man es beispielsweise für die rechnergestützte Mathematik benötigt), und in der Verifikation von Programmiersprachen mit Konstrukten höherer Stufe (funktionale Sprachen) eingesetzt werden.

• DFG-Verfahren: Sachbeihilfen
• Beteiligte Person: Professor Dr. Michael Kohlhase