Digital Proof Tools for Philosophical Logic

Formalisierung der Inhaltsgleichheit in der Wahrmachersemantik mit Lean 4 , von Menschen verfassten Beweisplänen und KI-gestützter Beweisentwicklung.

NWO Open Competition – XS 12 Monate

Digital Proof Tools for Philosophical Logic ist ein zwölfmonatiges Projekt, das untersucht, ob in der Mathematik entwickelte digitale Beweismethoden substanzielle Forschung in der philosophischen Logik unterstützen können.

Die technische Fallstudie ist das offene Problem der Charakterisierung bilateraler Äquivalenz (d. h. der Gleichheit von Wahrmachern und Falschmachern in allen Modellen) in der Wahrmachersemantik . Das Projekt wird den relevanten semantischen Rahmen in Lean formalisieren, die Beweissuche anhand eines von Menschen verfassten Beweisplans mit expliziten Abhängigkeiten steuern und Programmieragenten bewerten, indem ihre Ergebnisse sowohl mit Leans Kernel als auch anhand der vorgesehenen mathematischen Strategie überprüft werden. Ziel ist ein reproduzierbarer Arbeitsablauf, der philosophische Argumente, formale Aussagen, Beweissuche und verifizierte Beweisobjekte verbindet.

Meilensteine

  1. Forschungsstrategie und Beweisplan

    Geplant

    Ein Strategie-Repository pflegen, das einen mit leanblueprint erstellten Beweisplan mit expliziten Abhängigkeiten, von Menschen verfasste Beweisskizzen, Skills für KI-Agenten und Aufzeichnungen zum KI-gestützten Formalisierungsprozess enthält.

  2. Lean-Bibliothek für Wahrmachersemantik

    Geplant

    Die zentralen Definitionen und Ergebnisse zu Wahrmacherinhalten, Gegenstandsbereichen und thematischem Bezug in Lean 4 formalisieren, soweit möglich auf Mathlib aufbauen und die Bibliothek in einem öffentlichen GitHub -Repository bereitstellen.

  3. Digitale Beweisobjekte

    Geplant

    Vom Lean-Kernel geprüfte Dateien , abgeschlossene Knoten im Beweisplan und die zugehörige Dokumentation der Beweisentwicklung für das Charakterisierungsproblem erstellen.

  4. Publikationen und Ergebnisvermittlung

    Geplant

    Die logischen Ergebnisse und die methodologische Bewertung der KI-gestützten Beweisentwicklung in Fachartikeln und Konferenzvorträgen vorstellen.

Projektpartner