Det har visat sig att linjär logik kan användas som ett ramverk både för att ange bevissystem för ett antal logiker och för att visa grundläggande egenskaper hos de angivna systemen. Detta dokument visar hur man utvidgar ramen med subexponentiella för att förklara ett bredare spektrum av bevissystem, inklusive ett antal icke-triviala bevissystem som multi-conclusion intuitionistisk logik, klassisk modal logik S4, intuitionistisk Lax-logik, och Negris märkta bevissystem för olika modala logiker. Dessutom föreslår vi metoder för att kontrollera om ett kodat bevissystem har viktiga egenskaper, t.ex. om det medger cut-eliminering, fullständigheten i reglerna för atomisk identitet och dess invertibilitetsregler. Slutligen presenterar vi ett verktyg för att genomföra några av dessa specifikations-/verifieringsmetoder. 2 En utökad ram för att specificera och resonera om Proof Systems eftersom exponentiella i linjär logik är inte kanoniska [23, 7], Man kan konstruera linjär logik bevissystem som innehåller så många subexponentiella som ett behov. Denna funktion gjorde det möjligt att deklarativt koda ett brett spektrum av bevissystem, såsom ett multi-conclusion bevissystem för intuitionistisk logik [16]. Dessutom, eftersom den föreslagna kodningen är naturlig och direkt, kunde vi använda den rika linjära logiken meta-nivå teori för att resonera om de specificerade systemen på ett elegant och enkelt sätt. Bidraget från detta dokument är trefaldigt. Först, i Avsnitt 4, visar vi hur man deklarativt specificera bevissystem med mer involverade strukturella och logiska inferenser regler med linjär logik teorier med subexponentiella. Vi kodar bevissystem som har strukturella begränsningar som är mycket mer intressanta och utmanande än de system som anges i [26]. Förutom det multi-conclusion system för intuitionistisk logik som specificeras i vårt tidigare arbete, anger vi bevissystem för intuitionistisk slapp logik [10], fokuserad intuitionistisk logik LJQ *, klassisk modallogik S4 samt Negris märkta bevissystem för olika modala logiker. Dessa exempel ger belägg för att linjär logik med subexponentiella kan användas som en ram för ett antal bevissystem inklusive system för modal logik. Vårt andra bidrag, i avsnitt 5, följer och förstärker de idéer som presenteras i [19]. Vi tillhandahåller tillräckliga villkor för att garantera tre egenskaper hos system som anges med hjälp av subexponentiella: 1) tillåtligheten av cut-regeln; 2) fullständigheten av systemet när endast atomiska fall av den ursprungliga regeln; och 3) invertibiliteten av varje inference regel. Den största skillnaden från vad som presenteras här och det arbete som utvecklats under [19] är fastställandet av vissa kriterier för permutation av regler. En sådan analys behövs för att kontrollera om styckningsdelarna kan omvandlas till de viktigaste styckningsdelarna. Eftersom vårt ramverk möjliggör kodning av mycket mer komplicerade bevissystem, är beteendeanalysen mer involverad och det leder till mer allmänna villkor jämfört med [19]. Slutligen har vi implementerat ett verktyg, som beskrivs i avsnitt 6, som accepterar en linjär logik med subexponentiella specifikationer och automatiskt kontrollerar om principnedskärningar kan reduceras till atomnedskärningar och om de ursprungliga reglerna endast kan vara atomiska. Vårt verktyg kan visa att de flesta av de system som nämns 1 ovan uppfyller dessa villkor. Dessutom kan den kontrollera fall för när cut-rule kan permuteras över en introduktionsregel och när en introduktionsregel kan permutera över en annan introduktionsregel. En sådan analys kan i hög grad bidra till att upptäcka hörnfall för när minskningen av ett bevis med skärsår i ett bevis med huvudsakliga skärsår bara inte är omedelbar. Detta dokument är uppbyggt på följande sätt: I avsnitt 2 införs ett bevissystem för linjär logik med subexponentiella element, s.k. SELLF, som utgör grunden för det föreslagna logiska ramverket. I Avsnitt 3 beskriver vi hur man kodar ett bevissystem i vårt ramverk. I avsnitt 4 beskrivs kodning av ett antal bevissystem, nämligen bevissystemet G1m för minimal logik [33], det multi-conclusion proof-systemet för intuitionistisk logik mlJ [16], det fokuserade bevissystemet LJQ * för intuitionistisk logik [8], ett bevissystem för den klassiska modallogiken S4, ett bevissystem för intuitionistisk slapp logik [10] och det märkta bevissystemet G3K för modal logik [21]. I avsnitt 5 införs villkoren för att kontrollera om ett kodat bevissystem uppfyller de egenskaper som nämnts tidigare, vilket kan kontrolleras med hjälp av vårt verktyg som beskrivs i avsnitt 6. Slutligen avslutar vi i avsnitten 7 och 8 med att diskutera relaterat och framtida arbete. Detta är en förbättrad och utökad version av verkstadspapper [26]. 1 Undantaget är LJQ *, vars cut-eliminering argument är ganska inblandade. Även om vi antar att läsaren är bekant med linjär logik, granskar vi några av dess grundläggande bevisteori. Bokstäver är antingen atomformler (A) eller deras negationer (A). De bindväv och och deras enheter 1 och  till är multiplikativa; de bindväv och & och deras enheter 0 och är additiv;  och  på (första ordningen) kvantifier; och! och? är exponentiella (kallas bang respektive frågetecken). Vi kommer att anta att alla formler är i negation normal form, vilket innebär att alla negationer har atomisk räckvidd. På grund av exponentiella, kan man i linjär logik skilja två typer av formler: de linjära vars huvudsakliga bindväv inte är en? och de obundna vars viktigaste bindväv är en?. De linjära formlerna kan ses som resurser som bara kan användas en gång, medan de obundna formlerna representerar obegränsade resurser som kan användas så många gånger som behövs. Denna distinktion återspeglas vanligen i syntaxen genom att man använder två olika sammanhang i linjära logiska sekvenser (t.ex. en, som innehåller endast obundna formler och en annan (t.ex.) med endast linjära formler [1]. En sådan åtskillnad gör det möjligt att införliva strukturella regler, dvs. försvagning och sammandragning, i införandereglerna för bindväv, så som de görs i liknande presentationer för klassisk logik, t.ex. G3c-systemet i [33]. I en sådan presentation behandlas sammanhanget (-) som innehåller obundna formler som en uppsättning formler, medan det andra sammanhanget (-) som endast innehåller linjära formler behandlas som en multiuppsättning formler. Det visar sig att exponenterna inte är kanoniska [7] när det gäller det logiska ekvivalensförhållandet. I själva verket, om, av någon anledning, vi bestämmer oss för att definiera en blå och röd associationer (en b och en r respektive) med de vanliga klassiska reglerna: då är det lätt att visa att, för alla formler A och B, A  på b B. Detta innebär att alla symboler för klassisk förening tillhör samma ekvivalensklass. Därför kan vi välja att använda som förbindelsens kanoniska form någon särskild färg, och bevisbarhet påverkas inte av detta val. Men samma beteende håller inte med den linjära logiken exponentiellt. I själva verket, anta att vi har rött! Är det? R och blå! B,?..................................................................... b uppsättningar exponentiella med standardlinjära logikregler:
Nigam och Miller i [26] visade att det är möjligt att fånga ett bredare spektrum av bevissystem (följder, naturliga avdrag, tablåer, etc.) genom en generalisering av den typ av specifikationer som presenteras i detta dokument. Och i REF Nigam föreslog Pimentel och Reis att man skulle använda fokuserad linjär logik med subexponentiella element som metalogiska för att specificera bevissystem, tillsammans med en generalisering av begreppet samstämmighet som presenteras i detta dokument. Men det är värt att notera att även om subexponentialer möjliggör specificering av system på en nivå av fullständig härledning, blir det en svår uppgift att hitta allmänna villkor för att kontrollera egenskaper.
An extended framework for specifying and reasoning about proof systems
{'venue': 'J. Log. Comput.', 'journal': 'J. Log. Comput.', 'mag_field_of_study': ['Mathematics', 'Computer Science']}