Section Introduction

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

Sujets

• Herbrand's theorem
• Higher-order logic

Informations

• Publié par: chaeh
• Nombre de lectures: 13
• Langue: English

Extrait

Section1:Introduction 1:Introduction Mosttheoremprovingparadigmsforclassicallogicarecenteredaroundadhocproof structureswhicharedesignedtosupportaparticularsearchprocedure.Proofstructures, suchasresolutionrefutationsorconnectiongraphs,arenotintendedtobefirst-classvalues: theyareverylarge,implementationdependentstructureswhicharegenerallydiscarded aftertheirdiscovery.Thisisveryunfortunatesincethereismuchinformationwhich couldautomaticallybeextractfromsuchproofs.Suchtheoremproversare,forexample, incapableofrenderingnaturaljustificationsoftheirproofstoahumanreader. Oneobvioussolutiontothissituationistorepresentproofsbynaturaldeduction orsequentialprooftrees.Suchproofstructureshavebeenextensivelystudiedandmany structuralmanipulationsareknown.Thereare,however,atleasttwodrawbackstousing suchprooftreesinaclassicallogicsetting.First,suchtreesarealsoverylargeandawkward objectsbecausetheycontainfarmoreexplicitinformationthanisgenerallyofinterest. Forexample,naturaldeductionproofsrecordtheorderinwhicheverylogicalconnective andquantifierisintroducedandeliminated.Secondly,Herbrand’sTheoremstatesthat itissubstitutionwhichisthekeyelementinclassicalproofs;logicalconnectivesplaya secondaryandsimplierrole.Hence,itshouldbepossibletogreatlysimplifyrepresentation ofproofsinclassicallogicbysimplyrecordingtherolesubstitutionsplayinbuildingproofs. Inthispaper,wepresentjustsucharepresentationforclassicalproofs,calledex- pansiontreeproofs.Theseproofstructuresrecordinaverycompactformtheessential information,namelysubstitutions,ofclassicalproofs.Wefeelthatthesestructuresmake suitablevalueswithincomputationalsettings,andwedemonstratethisbypresentingsev- eralcomputationswhichcanbeperformeddirectlyonthem.Inparticular,weshowhowto convertexpansiontreeproofstoH-proofs[8](derivationsfromtautologiesusinguniversal andexistentialgeneralization),cut-freesequentialproofs[7,13,16],andlinearreasoning [5].Inthelattersystem,wheninterpolantsexist,averysimplecomputationonexpan- siontreeproofswillproducethem.Finally,sincemanyclassicallogicproofsystemsare designedtouseSkolemtermstosimplifytheroleofquantifiersinproofs,wepresenta versionofexpansiontreeswhichuseSkolemterms.Weshowthatthesetwoversionare equivalentbypresentingthetransformationsbetweenthem. Fortraditionaltheoremprovingsystems,theconversionofexpansiontreeproofsto sequentialproofsisveryvaluable.Inparticular,ifagivenresolution-styletheoremprover builtanexpansiontreefromitsresolutionrefutation,thetransformationtothe“natural” proofstructuresdescribedinSection4wouldprovideameansbywhichahumanreadable presentationofaresolutionrefutationcouldbegenerated.Justsuchapracticaluseof expansiontreeproofshasbeendemonstratedin[6,11]. Sincesubstitutionsarecentraltounderstandingclassicalproofsandsincetheλ- calculusisanelegantformalismforrepresentingsubstitutions,wehavechoosetouse –1–

2:LogicalPreliminaries aversionofclassicallogicwhichisbasedonChurch’sSimpleTheoryofTypes[3].This logiccanrepresentquantificationatallfinitetypes,and,hence,alltheresultsofthispaper arevalidforhigher-orderlogicaswellasforfirst-orderlogic.Furthermore,wehavebeen abletoprovidetworesultsforthishigher-orderlogicwhichhavenotappearedbeforein theliterature:astrengthenedformofthe(first-order)interpolationtheorem,andacorrect descriptionofSkolemfunctionsandtheHerbrandUniverse. Section2:LogicalPreliminaries Thehigher-orderlogic,T,whichweshallconsiderhereisessentiallytheSimpleTheory ofTypesdescribedbyChurchin[3],exceptthatwedonotusetheaxiomsofextension- ality,choice,descriptions,orinfinity.Tcontainstwobasetypes,oforbooleanandιfor individuals,althoughaddinganynumberofotherbasetypescaneasilybedone.Allother typesarefunctionaltypes,i.e.thetype(βα)isthetypeofafunctionwithdomaintype αandcodomaintypeβ.Suchtypesareoftenwrittenelsewhereasα→β.Thetype (oα),beingthetypeofafunctionfromtypeαtobooleans,i.e.acharacteristicfunction, isusedinTtorepresentthetypeforsetsandpredicatesofelementsoftypeα.Formulas arebuiltupfromlogicalconstants,variables,andparameters(nonlogicalconstants)byλ- abstractionandfunctionapplication.Hence,thetypeof[λx α A β ](wherex α isavariable) is(βα)whilethetypefor[A (βα) B α ]isβ.(Here,typesubscriptsprovidefortypeassign- ments.)Weshallseldomadornformulaswithtypesymbols,butrather,whenthetypeof aformula,sayA,cannotbedeterminedfromcontext,wewilladdthephrase“whereAis aformula α (variable α )(constant α )”toindicatethatAhastypeα.Whenwedoprovides typesassubscriptswithinlargerformulas,weshallonlyprovideanexplicittypeforthe firstoccurrenceofavariableorconstant—weshallassumethatallotheroccurrences willbeimplicitlytypedthesame.ThelogicalconstantsofTare∼ oo (negation),∨ (oo)o (disjunction),and,foreachtypeα,∀ o(oα) (the“universalα-typesetrecognizer”).Wealso usethefollowingabbreviations:A∧Bstandsfor∼[∼A∨∼B],A⊃Bstandsfor∼A∨B, ∀xPstandsfor∀[λxP],and∃xPstandsfor∼∀[λx∼P].Sincethetypeofasetisofthe form(oα),wewriteL oα x α todenotetheset-theoreticexpressionx∈L. Weshallpresentafewsimplefactsaboutλ-conversion.Thereaderisreferredto[3] and[4]formoredetails.Ifxisavariable α andtisaformula α ,S . t x Adenotestheformula whichistheresultofreplacingallfreeoccurrencesofxinAwitht.Weshallassumethat boundvariablenamesaresystematicallychangedtoavoidvariablecapture.Theoperation ofreplacingasubformulaofAoftheform[λxC]EwithS . x E Ciscalledλ-contraction.We writeAredBifBistheresultofzeroormorealphabeticchangesinboundvariablesand λ-contractionsofA.Theconverseofλ-contractionisλ-expansion.WewriteAconvB andsaythatAisλ-convertibletoBifBistheresultofzeroormorealphabeticchanges inboundvariables,λ-contractions,andλ-expansions.Aformulaisinλ-normalformif itcontainsnocontractiblepart,i.e.asubformulaoftheform[λxC]E.Foreverytyped –2–