Digital Proof Tools for Philosophical Logic is een project van twaalf maanden dat onderzoekt of digitale bewijsmethoden uit de wiskunde inhoudelijk onderzoek in de filosofische logica kunnen ondersteunen.
De technische casestudy betreft het open probleem van de karakterisering van bilaterale equivalentie (d.w.z. dezelfde waarmakers en onwaarmakers in alle modellen) in de waarmakersemantiek . Het project zal het relevante semantische raamwerk formaliseren in Lean , het zoeken naar bewijzen sturen met een door mensen opgestelde bewijsblauwdruk waarin afhankelijkheden expliciet zijn vastgelegd, en programmeeragenten evalueren door hun resultaten te toetsen aan zowel de kernel van Lean als de beoogde wiskundige strategie. Het doel is een reproduceerbare werkwijze die filosofische argumenten, formele uitspraken, het zoeken naar bewijzen en geverifieerde bewijsobjecten met elkaar verbindt.
Mijlpalen
Onderzoeksstrategie en bewijsblauwdruk
Gepland
Een strategierepository bijhouden met een inleanblueprintgemaakte bewijsblauwdruk waarin afhankelijkheden expliciet zijn vastgelegd, door mensen geschreven bewijsplannen, skills voor AI-agenten en verslagen van het AI-ondersteunde formaliseringsproces.Digitale bewijsobjecten
Gepland
Door de Lean-kernel gecontroleerde bestanden , voltooide knooppunten in de bewijsblauwdruk en de bijbehorende documentatie van de bewijsontwikkeling voor het karakteriseringsprobleem opleveren.Publicaties en kennisverspreiding
Gepland
De logische resultaten en de methodologische beoordeling van AI-ondersteunde bewijsontwikkeling presenteren in wetenschappelijke artikelen en conferentiebijdragen.