Section Introduction

pages

English

Documents

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

chaeh

Nombre de lectures

Langue

English

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

Voir

Publié par

chaeh

Nombre de lectures

Langue

English

Herbrand's theorem Higher-order logic

Section1:Introduction1:IntroductionMosttheoremprovingparadigmsforclassicallogicarecenteredaroundadhocproofstructureswhicharedesignedtosupportaparticularsearchprocedure.Proofstructures,suchasresolutionrefutationsorconnectiongraphs,arenotintendedtobeﬁrst-classvalues:theyareverylarge,implementationdependentstructureswhicharegenerallydiscardedaftertheirdiscovery.Thisisveryunfortunatesincethereismuchinformationwhichcouldautomaticallybeextractfromsuchproofs.Suchtheoremproversare,forexample,incapableofrenderingnaturaljustiﬁcationsoftheirproofstoahumanreader.Oneobvioussolutiontothissituationistorepresentproofsbynaturaldeductionorsequentialprooftrees.Suchproofstructureshavebeenextensivelystudiedandmanystructuralmanipulationsareknown.Thereare,however,atleasttwodrawbackstousingsuchprooftreesinaclassicallogicsetting.First,suchtreesarealsoverylargeandawkwardobjectsbecausetheycontainfarmoreexplicitinformationthanisgenerallyofinterest.Forexample,naturaldeductionproofsrecordtheorderinwhicheverylogicalconnectiveandquantiﬁerisintroducedandeliminated.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,sincemanyclassicallogicproofsystemsaredesignedtouseSkolemtermstosimplifytheroleofquantiﬁersinproofs,wepresentaversionofexpansiontreeswhichuseSkolemterms.Weshowthatthesetwoversionareequivalentbypresentingthetransformationsbetweenthem.Fortraditionaltheoremprovingsystems,theconversionofexpansiontreeproofstosequentialproofsisveryvaluable.Inparticular,ifagivenresolution-styletheoremproverbuiltanexpansiontreefromitsresolutionrefutation,thetransformationtothe“natural”proofstructuresdescribedinSection4wouldprovideameansbywhichahumanreadablepresentationofaresolutionrefutationcouldbegenerated.Justsuchapracticaluseofexpansiontreeproofshasbeendemonstratedin[6,11].Sincesubstitutionsarecentraltounderstandingclassicalproofsandsincetheλ-calculusisanelegantformalismforrepresentingsubstitutions,wehavechoosetouse–1–

2:LogicalPreliminariesaversionofclassicallogicwhichisbasedonChurch’sSimpleTheoryofTypes[3].Thislogiccanrepresentquantiﬁcationatallﬁnitetypes,and,hence,alltheresultsofthispaperarevalidforhigher-orderlogicaswellasforﬁrst-orderlogic.Furthermore,wehavebeenabletoprovidetworesultsforthishigher-orderlogicwhichhavenotappearedbeforeintheliterature:astrengthenedformofthe(ﬁrst-order)interpolationtheorem,andacorrectdescriptionofSkolemfunctionsandtheHerbrandUniverse.Section2:LogicalPreliminariesThehigher-orderlogic,T,whichweshallconsiderhereisessentiallytheSimpleTheoryofTypesdescribedbyChurchin[3],exceptthatwedonotusetheaxiomsofextension-ality,choice,descriptions,orinﬁnity.Tcontainstwobasetypes,oforbooleanandιforindividuals,althoughaddinganynumberofotherbasetypescaneasilybedone.Allothertypesarefunctionaltypes,i.e.thetype(βα)isthetypeofafunctionwithdomaintypeαandcodomaintypeβ.Suchtypesareoftenwrittenelsewhereasα→β.Thetype(oα),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,weshallonlyprovideanexplicittypefortheﬁrstoccurrenceofavariableorconstant—weshallassumethatallotheroccurrenceswillbeimplicitlytypedthesame.ThelogicalconstantsofTare∼oo(negation),∨(oo)o(disjunction),and,foreachtypeα,∀o(oα)(the“universalα-typesetrecognizer”).Wealsousethefollowingabbreviations:A∧Bstandsfor∼[∼A∨∼B],A⊃Bstandsfor∼A∨B,∀xPstandsfor∀[λxP],and∃xPstandsfor∼∀[λx∼P].Sincethetypeofasetisoftheform(oα),wewriteLoαxαtodenotetheset-theoreticexpressionx∈L.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.Foreverytyped–2–

Voir

Univers
Ebooks
Livres audio
Presse
Podcasts
BD
Documents

Section Introduction

YouScribe

Le catalogue

Le service

Les conditions