Qatar November

Description

Niveau: Supérieur
Qatar, 22 November 2008 1/28 A range of object-level proof systems from focusing a linear logical framework Dale Miller INRIA - Saclay & LIX, Ecole Polytechnique Outline 1. Basics: linear logic and focused proofs 2. A word about object-logic / meta-logic 3. Assigning polarities to atoms 4. Specification of various object-level proof systems Joint work with Vivek Nigam. Based on a paper in IJCAR 2008.

• connective


• linear logic


• derived using theory


• introduction rules


• arrow ?


• arrow ?


• negation normal

Sujets

• École polytechnique
• Connective
• Linear logic

Informations

• Publié par: chaeh
• Nombre de lectures: 26

Extrait

Qatar,22November2008 Arangeofobject-levelproofsystems morf focusingalinearlogicalframework DaleMiller INRIA-Saclay&LIX,EcolePolytechnique Outline 1.Basics:linearlogicandfocusedproofs 2.Awordaboutobject-logic/meta-logic 3.Assigningpolaritiestoatoms 4.Specificationofvariousobject-levelproofsystems Jointworkwith.8002RACJInirepapanodesaB.magiNkeviV 182/

Qatar,22November2008 ReviewofLinearLogic Literalsareeitheratomicformulasortheirnegations. 2/28 Wewrite¬BtodenotethenegationnormalformoftheformulaB: usedeMorgandualitiestopushnegationtohaveonlyatomic scope. Theconnectives⊗andOandtheirunits1and⊥are multiplicative;theconnectives⊕and&andtheirunits0and>are additiveconnectives;∀and∃are(first-order)quantifiers;and!and ?aretheexponentials. B≡Ctodenotestheformula(¬BOC)&(¬COB). TheformulaBisderivedusingtheoryXif`B,?Xisprovablein linearlogic.