Bevisnät

I bevisteorin är bevisnät en geometrisk metod för att representera bevis som eliminerar två former av byråkrati som skiljer på bevis: (A) irrelevanta syntaktiska egenskaper hos vanliga beviskalkyler och (B) ordningen på regler som tillämpas i en härledning. På så sätt motsvarar bevisidentitetens formella egenskaper närmare de intuitivt önskvärda egenskaperna. Provnät introducerades av Jean-Yves Girard . Detta skiljer bevisnät från vanliga beviskalkyler som den naturliga deduktionskalkylen och den efterföljande kalkylen, där dessa fenomen finns.

Till exempel är dessa två linjära logiska bevis identiska:

$\vdash$ A , B , C , D $\vdash$ A ⅋ B , C , D $\vdash$ A ⅋ B , C ⅋ D

$\vdash$ A , B , C , D $\vdash$ A , B , C ⅋ D $\vdash$ A ⅋ B , C ⅋ D

Och deras motsvarande nät kommer att vara desamma.

Riktighetskriterier

Flera korrekthetskriterier är kända för att kontrollera om en sekventiell bevisstruktur (dvs något som verkar vara ett bevisnät) faktiskt är en konkret bevisstruktur (dvs något som kodar en giltig härledning i linjär logik). Det första sådana kriteriet är kriteriet för långa resor som beskrevs av Jean-Yves Girard .

Se även

• Linjär logik
• Ludics
• Interaktionens geometri
• Sammanhängande utrymme
• Djup slutledning
• Interaktionsnät

Källor

• Bevis och typer . Girard JY, Lafont Y, och Taylor P. Cambridge Press, 1989.
• Roberto Di Cosmo och Vincent Danos, The Linear Logic Primer
• Sean A. Fulop, En undersökning av bevisnät och matriser för substrukturell logik