I detta dokument föreslås en enhetlig metod för att utföra naturlig avledning över familjen av linjära, relevanta och intuitionistiska logiker. Metoden följer disciplinen LDS (Labelled Deductive Systems), där deduktiva processen manipulerar deklarativa enheter -formler märkta enligt en märkning algebra. I det system som beskrivs här är etiketter antingen marktermer eller variabler i ett visst märkningsspråk, och inferensreglerna manipulerar formler och etiketter samtidigt, vilket skapar (vid behov) begränsningar på de etiketter som används i reglerna. En uppsättning naturliga avdrag stil inference regler ges, och begreppet härledning definieras som associerar en märkt naturlig avdrag stil "strukturell härledning" med en uppsättning genererade begränsningar. Algoritmiska förfaranden, baserade på en teknik som kallas resurs bortförande, definieras för att lösa de begränsningar som genereras inom en härledning, och deras uppsägningsvillkor diskuteras. En naturlig härledning är korrekt med avseende på en given substrukturell logik, om, under förutsättning att algoritmiska förfaranden avslutas, den tillhörande uppsättningen begränsningar är uppfyllda med avseende på den underliggande märkningen algebra. Detta visar sig genom att bevisa att det naturliga avdragssystemet är sunt och fullständigt när det gäller LKE-tabellaux-systemet [DG94].
Det bör också nämnas att märkta avdragssystem utgör grunden för de naturliga avdragssystem för substrukturella logiker som ges i REF.
Labelled Natural Deduction for Substructural Logics
{'venue': 'Logic Journal of the IGPL', 'journal': None, 'mag_field_of_study': ['Computer Science', 'Mathematics']}