Digital Proof Tools for Philosophical Logic

Formalizzare l’identità di contenuto nella semantica dei verificatori con Lean 4, piani di dimostrazione redatti da persone e sviluppo di dimostrazioni assistito dall’IA.

NWO Open Competition – XS 12 mesi

Digital Proof Tools for Philosophical Logic è un progetto di dodici mesi che verifica se i metodi digitali di dimostrazione sviluppati in matematica possano sostenere la ricerca sostanziale in logica filosofica.

Il caso di studio tecnico è il problema aperto della caratterizzazione dell’equivalenza bilaterale (ossia l’identità dei verificatori e dei falsificatori in tutti i modelli) nella semantica dei verificatori. Il progetto formalizzerà il quadro semantico pertinente in Lean, utilizzerà un piano di dimostrazione redatto da persone e con dipendenze esplicite per guidare la ricerca delle dimostrazioni, e valuterà gli agenti di programmazione verificandone i risultati sia con il kernel di Lean sia rispetto alla strategia matematica prevista. L’obiettivo è un processo riproducibile che colleghi argomenti filosofici, enunciati formali, ricerca delle dimostrazioni e oggetti di dimostrazione verificati.

Tappe del progetto

  1. Strategia di ricerca e piano di dimostrazione

    In programma

    Mantenere un repository di strategia contenente un piano di dimostrazione creato con leanblueprint che espliciti le dipendenze, schemi dimostrativi redatti da persone, skill per agenti IA e documentazione del processo di formalizzazione assistito dall’IA.

  2. Libreria Lean per la semantica dei verificatori

    In programma

    Formalizzare in Lean 4 le definizioni e i risultati fondamentali sul contenuto nella semantica dei verificatori, sull’argomento e sulla relazione di pertinenza tematica, utilizzando Mathlib ove possibile, e pubblicare la libreria in un repository GitHub pubblico.

  3. Oggetti di dimostrazione digitali

    In programma

    Produrre file Lean verificati dal kernel, nodi completati del piano di dimostrazione e la relativa documentazione dello sviluppo delle dimostrazioni per il problema di caratterizzazione.

  4. Pubblicazioni e divulgazione dei risultati

    In programma

    Presentare i risultati logici e la valutazione metodologica dello sviluppo di dimostrazioni assistito dall’IA in articoli specialistici e interventi a convegni.

Collaboratori