Gleichheitsbeweisen höherer Stufe

• Applicant: Professor Dr. Jörg H. Siekmann
• Subject Area: Theoretical Computer Science
• Term: from 1996 to 2003
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Grants
• Participating Person: Professor Dr. Michael Kohlhase