Section Introduction
24 Pages
English
Gain access to the library to view online
Learn more

Section Introduction

Gain access to the library to view online
Learn more
24 Pages
English

Description

Niveau: Supérieur
1: Introduction Section 1: Introduction Most theorem proving paradigms for classical logic are centered around ad hoc proof structures which are designed to support a particular search procedure. Proof structures, such as resolution refutations or connection graphs, are not intended to be first-class values: they are very large, implementation dependent structures which are generally discarded after their discovery. This is very unfortunate since there is much information which could automatically be extract from such proofs. Such theorem provers are, for example, incapable of rendering natural justifications of their proofs to a human reader. One obvious solution to this situation is to represent proofs by natural deduction or sequential proof trees. Such proof structures have been extensively studied and many structural manipulations are known. There are, however, at least two drawbacks to using such proof trees in a classical logic setting. First, such trees are also very large and awkward objects because they contain far more explicit information than is generally of interest. For example, natural deduction proofs record the order in which every logical connective and quantifier is introduced and eliminated. Secondly, Herbrand's Theorem states that it is substitution which is the key element in classical proofs; logical connectives play a secondary and simplier role. Hence, it should be possible to greatly simplify representation of proofs in classical logic by simply recording the role substitutions play in building proofs. In this paper, we present just such a representation for classical proofs, called ex- pansion tree proofs.

  • such proof

  • structures make

  • skolem functions

  • herbrand's theorem

  • can easily

  • higher-order logic

  • normal formulao?

  • such


Subjects

Informations

Published by
Reads 13
Language English

Exrait

Section1:Introduction1:IntroductionMosttheoremprovingparadigmsforclassicallogicarecenteredaroundadhocproofstructureswhicharedesignedtosupportaparticularsearchprocedure.Proofstructures,suchasresolutionrefutationsorconnectiongraphs,arenotintendedtobefirst-classvalues:theyareverylarge,implementationdependentstructureswhicharegenerallydiscardedaftertheirdiscovery.Thisisveryunfortunatesincethereismuchinformationwhichcouldautomaticallybeextractfromsuchproofs.Suchtheoremproversare,forexample,incapableofrenderingnaturaljustificationsoftheirproofstoahumanreader.Oneobvioussolutiontothissituationistorepresentproofsbynaturaldeductionorsequentialprooftrees.Suchproofstructureshavebeenextensivelystudiedandmanystructuralmanipulationsareknown.Thereare,however,atleasttwodrawbackstousingsuchprooftreesinaclassicallogicsetting.First,suchtreesarealsoverylargeandawkwardobjectsbecausetheycontainfarmoreexplicitinformationthanisgenerallyofinterest.Forexample,naturaldeductionproofsrecordtheorderinwhicheverylogicalconnectiveandquantifierisintroducedandeliminated.Secondly,Herbrand’sTheoremstatesthatitissubstitutionwhichisthekeyelementinclassicalproofs;logicalconnectivesplayasecondaryandsimplierrole.Hence,itshouldbepossibletogreatlysimplifyrepresentationofproofsinclassicallogicbysimplyrecordingtherolesubstitutionsplayinbuildingproofs.Inthispaper,wepresentjustsucharepresentationforclassicalproofs,calledex-pansiontreeproofs.Theseproofstructuresrecordinaverycompactformtheessentialinformation,namelysubstitutions,ofclassicalproofs.Wefeelthatthesestructuresmakesuitablevalueswithincomputationalsettings,andwedemonstratethisbypresentingsev-eralcomputationswhichcanbeperformeddirectlyonthem.Inparticular,weshowhowtoconvertexpansiontreeproofstoH-proofs[8](derivationsfromtautologiesusinguniversalandexistentialgeneralization),cut-freesequentialproofs[7,13,16],andlinearreasoning[5].Inthelattersystem,wheninterpolantsexist,averysimplecomputationonexpan-siontreeproofswillproducethem.Finally,sincemanyclassicallogicproofsystemsaredesignedtouseSkolemtermstosimplifytheroleofquantifiersinproofs,wepresentaversionofexpansiontreeswhichuseSkolemterms.Weshowthatthesetwoversionareequivalentbypresentingthetransformationsbetweenthem.Fortraditionaltheoremprovingsystems,theconversionofexpansiontreeproofstosequentialproofsisveryvaluable.Inparticular,ifagivenresolution-styletheoremproverbuiltanexpansiontreefromitsresolutionrefutation,thetransformationtothe“natural”proofstructuresdescribedinSection4wouldprovideameansbywhichahumanreadablepresentationofaresolutionrefutationcouldbegenerated.Justsuchapracticaluseofexpansiontreeproofshasbeendemonstratedin[6,11].Sincesubstitutionsarecentraltounderstandingclassicalproofsandsincetheλ-calculusisanelegantformalismforrepresentingsubstitutions,wehavechoosetouse1
2:LogicalPreliminariesaversionofclassicallogicwhichisbasedonChurch’sSimpleTheoryofTypes[3].Thislogiccanrepresentquantificationatallfinitetypes,and,hence,alltheresultsofthispaperarevalidforhigher-orderlogicaswellasforfirst-orderlogic.Furthermore,wehavebeenabletoprovidetworesultsforthishigher-orderlogicwhichhavenotappearedbeforeintheliterature:astrengthenedformofthe(first-order)interpolationtheorem,andacorrectdescriptionofSkolemfunctionsandtheHerbrandUniverse.Section2:LogicalPreliminariesThehigher-orderlogic,T,whichweshallconsiderhereisessentiallytheSimpleTheoryofTypesdescribedbyChurchin[3],exceptthatwedonotusetheaxiomsofextension-ality,choice,descriptions,orinfinity.Tcontainstwobasetypes,oforbooleanandιforindividuals,althoughaddinganynumberofotherbasetypescaneasilybedone.Allothertypesarefunctionaltypes,i.e.thetype(βα)isthetypeofafunctionwithdomaintypeαandcodomaintypeβ.Suchtypesareoftenwrittenelsewhereasαβ.Thetype(),beingthetypeofafunctionfromtypeαtobooleans,i.e.acharacteristicfunction,isusedinTtorepresentthetypeforsetsandpredicatesofelementsoftypeα.Formulasarebuiltupfromlogicalconstants,variables,andparameters(nonlogicalconstants)byλ-abstractionandfunctionapplication.Hence,thetypeof[λxαAβ](wherexαisavariable)is(βα)whilethetypefor[A(βα)Bα]isβ.(Here,typesubscriptsprovidefortypeassign-ments.)Weshallseldomadornformulaswithtypesymbols,butrather,whenthetypeofaformula,sayA,cannotbedeterminedfromcontext,wewilladdthephrase“whereAisaformulaα(variableα)(constantα)”toindicatethatAhastypeα.Whenwedoprovidestypesassubscriptswithinlargerformulas,weshallonlyprovideanexplicittypeforthefirstoccurrenceofavariableorconstant—weshallassumethatallotheroccurrenceswillbeimplicitlytypedthesame.ThelogicalconstantsofTareoo(negation),(oo)o(disjunction),and,foreachtypeα,o()(the“universalα-typesetrecognizer”).Wealsousethefollowingabbreviations:ABstandsfor[A∨∼B],ABstandsforAB,xPstandsfor[λxP],andxPstandsfor∼∀[λxP].Sincethetypeofasetisoftheform(),wewriteLxαtodenotetheset-theoreticexpressionxL.Weshallpresentafewsimplefactsaboutλ-conversion.Thereaderisreferredto[3]and[4]formoredetails.Ifxisavariableαandtisaformulaα,S.txAdenotestheformulawhichistheresultofreplacingallfreeoccurrencesofxinAwitht.Weshallassumethatboundvariablenamesaresystematicallychangedtoavoidvariablecapture.TheoperationofreplacingasubformulaofAoftheform[λxC]EwithS.xECiscalledλ-contraction.WewriteAredBifBistheresultofzeroormorealphabeticchangesinboundvariablesandλ-contractionsofA.Theconverseofλ-contractionisλ-expansion.WewriteAconvBandsaythatAisλ-convertibletoBifBistheresultofzeroormorealphabeticchangesinboundvariables,λ-contractions,andλ-expansions.Aformulaisinλ-normalformifitcontainsnocontractiblepart,i.e.asubformulaoftheform[λxC]E.Foreverytyped2