Using linear logic to reason about sequent systems

Elaine Pimentel2

Description

Niveau: Supérieur, Doctorat, Bac+8
Using linear logic to reason about sequent systems ? Dale Miller1 and Elaine Pimentel2 1 Computer Science and Engineering Department, 220 Pond Lab, Pennsylvania State University, University Park, PA 16802-6106 USA 2 Departamento de Matematica, Universidade Federal de Minas Gerais, Belo Horizonte, M.G. Brasil Abstract. Linear logic can be used as a meta-logic for the specifica- tion of some sequent calculus proof systems. We explore in this paper properties of such linear logic specifications. We show that derivability of one proof system from another has a simple decision procedure that is implemented simply via bounded logic programming search. We also provide conditions to ensure that an encoded proof system has the cut- elimination property and show that this can be decided again by simple, bounded proof search algorithms. 1 Introduction Various logical frameworks based on intuitionistic logic have been proposed [FM88,Pau89,HHP93] and used for specifying natural deduction proof systems. Given the intimate connection between natural deduction and ?-calculus, appli- cations requiring object-level binding and substitutions have also been success- fully implemented in these logical frameworks [Mil00]. In [Mil96], Miller proposed moving from intuitionistic logic to the more ex- pressive setting of linear logic to capture the more general setting of sequent calculus proof system.

• linear logic


• flat forum


• forum


• proof system


• proof systems


• contraction can


• sequents within


• forum sequent

Sujets

• Pennsylvania State University
• Linear logic

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 95
• Langue: English

Extrait

Usinglinearlogictoreasonaboutsequent systems ? DaleMiller 1 andElainePimentel 2 1 ComputerScienceandEngineeringDepartment,220PondLab, PennsylvaniaStateUniversity,UniversityPark,PA16802-6106USA [e-mail] 2 DepartamentodeMatema´tica, UniversidadeFederaldeMinasGerais,BeloHorizonte,M.G.Brasil [e-mail] Abstract.Linearlogiccanbeusedasameta-logicforthespecifica- tionofsomesequentcalculusproofsystems.Weexploreinthispaper propertiesofsuchlinearlogicspecifications.Weshowthatderivability ofoneproofsystemfromanotherhasasimpledecisionprocedurethat isimplementedsimplyviaboundedlogicprogrammingsearch.Wealso provideconditionstoensurethatanencodedproofsystemhasthecut- eliminationpropertyandshowthatthiscanbedecidedagainbysimple, boundedproofsearchalgorithms. 1Introduction Variouslogicalframeworksbasedonintuitionisticlogichavebeenproposed [FM88,Pau89,HHP93]andusedforspecifyingnaturaldeductionproofsystems. Giventheintimateconnectionbetweennaturaldeductionandλ-calculus,appli- cationsrequiringobject-levelbindingandsubstitutionshavealsobeensuccess- fullyimplementedintheselogicalframeworks[Mil00]. In[Mil96],Millerproposedmovingfromintuitionisticlogictothemoreex- pressivesettingoflinearlogictocapturethemoregeneralsettingofsequent calculusproofsystem.Thisuseoflinearlogichasbeenfutureexploredin [Ric98,Pim01,MP].InthispaperweconsiderthestructureofproofsintheForum presentationoflinearlogicinordertoshowhowvariousaspectsofthemeta- theoryoflinearlogiccanbeusedtoconcludepropertiesofthesequentcalculus beingspecified.Inparticular,wedescribeadecisionprocedurefordetermining ifoneencodedproofsystemisderivablefromanotherandwepresentconditions andtheirdecisionprocedurethatimplythatanencodedproofsystemsatisfies cut-elimination. AfterprovidinganoverviewofForuminSection2andtheencodinginto Forumofobject-levelsequentsandinferencerulesinSection3,weprovein ? MillerhasbeensupportedinpartbyNSFgrantsCCR-9912387,CCR-9803971,INT- 9815645,andINT-9815731.BothauthorswishtothankL’InstitutdeMathe´matiques deLuminy,UniversityAix-Marseille2forthesupporttoattendtheLogicandIn- teractionWeeksinFebruary2002,duringwhichmuchofthispaperwaswritten.

Section4thatdeductionbetweenencodingsofinferencerulesiscapturedby shallowForumproofs.Adecisionprocedurefordeterminingiftheencoding ofoneproofsystemisderivablefromanotherproofsystemthenfollowsby doingboundeddepthproofsearch.Ofcourse,wewishtoknowifanobject-level proofsystemadmitsacut-eliminationtheorem.Section5containsthebasic backgroundforthisproblemandSection6containsthemainobject-levelcut- eliminationtheorem.Section7containsaspecificationanddiscussionofGirard’s LogicofUnity.Finally,weconcludeinSection8. 2TheForumpresentationoflinearlogic TheForumpresentationoflinearlogic[Mil96]reliesontheconnectives⊥, . ,?, >,&,−◦,⇒,and∀:thissetofconnectivesiscompleteforlinearlogic,inthesense thatallotherlinearlogicconnectivescanbedefinedfromthese.Proofsearch usingthiscollectionofconnectivescanberestrictedsothatsimplegoal-directed proofsearch(usingthetechnicaldeviceofmultiple-conclusionuniformproofs [Mil93])iscomplete.Thus,Forummakesitpossibletoclaimthatalloflinear logiccanbeseenasanabstractlogicprogramminglanguage[MNPS91].Forum hasbeenusedtospecifyanumberofcomputationsystems,rangingfromobject- orientedlanguages[DM95],imperativeprogrammingfeatures[Mil96,Chi95],and aRISCprocessor[Chi95].Inthispaper,weuseForumasaspecificationlanguage forsequentcalculusproofsystems.Forthispurpose,weworkoftenwithina weakerfragmentofForum,calledFlatForum. 2.1FlatForum AformulaofForumisaflatgoalifitdoesnotcontainoccurrencesof−◦and⇒, andalloccurrencesofthemodal?haveatomicscope.Aformulaoftheform ∀y¯(G 1 ,→∙∙∙,→G m ,→A 1 . ∙∙∙ . A n ),(m,n≥0) iscalledaflatclauseifG 1 ,...,G m areflatgoals,A 1 ,...,A n areatomicformulas, andoccurrencesofthesymbol,→areeitheroccurrencesof−◦or⇒.Theformula A 1 . ∙∙∙ . A n istheheadofsuchaclause,whileforeachi=1,...,m,the formulaG i isabodyofthisclause.Ifn=0,thenwewritetheheadassimply⊥ andsaythattheheadisempty.AflatclauseisessentiallyaclauseoftheLinLog system[And92]exceptthatheadsofflatclausesmaybeempty. AflatForumformulaislogicallyequivalenttoaformulainuncurriedform, namely,aformulaoftheform ∀y¯(B−◦A 1 . ∙∙∙ . A n ) wheren≥0,y¯isthelistofvariablesfreeintheheadA 1 . ∙∙∙ . A n ,allfree variablesofBarealsofreeinthehead,andBmayhaveoccurrencesof∃,⊗, 1,and!,butnotinthescopeof . ,?,&,∀,−◦,and⇒(usingtheterminology