Incorporating tables into proofs

Description

Niveau: Supérieur, Doctorat, Bac+8
Incorporating tables into proofs Dale Miller and Vivek Nigam INRIA & LIX/Ecole Polytechnique, Palaiseau, France nigam at lix.inria.fr dale.miller at inria.fr Abstract. We consider the problem of automating and checking the use of previously proved lemmas in the proof of some main theorem. In particular, we call the collection of such previously proved results a table and use a partial order on the table's entries to denote the (provability) dependency relationship between tabled items. Tables can be used in au- tomated deduction to store previously proved subgoals and in interactive theorem proving to store a sequence of lemmas introduced by a user to direct the proof system towards some final theorem. Tables of literals can be incorporated into sequent calculus proofs using two ideas. First, cuts are used to incorporate tabled items into a proof: one premise of the cut requires a proof of the lemma and the other branch of the cut inserts the lemma into the set of assumptions. Second, to ensure that lemma is not reproved, we exploit the fact that in focused proofs, atoms can have different polarity. Using these ideas, simple logic engines that do focused proof search (such as logic programming interpreters) are able to check proofs for correctness with guarantees that previous work is not redone. We also discuss how a table can be seen as a proof object and discuss some possible uses of tables-as-proofs.

• goal


• intuitionistic logic


• original conjunctive


• proved


• table can


• main connective


• a4 ?


• path a3


• logic programming systems

Sujets

• École polytechnique
• Intuitionistic logic

Informations

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

Extrait

Incorporatingtablesintoproofs DaleMillerandVivekNigam INRIA&LIX/E ´ colePolytechnique,Palaiseau,France nigamatlix.inria.frdale.milleratinria.fr Abstract. Weconsidertheproblemofautomatingandcheckingthe useofpreviouslyprovedlemmasintheproofofsomemaintheorem.In particular,wecallthecollectionofsuchpreviouslyprovedresultsatable anduseapartialorderonthetable’sentriestodenotethe(provability) dependencyrelationshipbetweentableditems.Tablescanbeusedinau- tomateddeductiontostorepreviouslyprovedsubgoalsandininteractive theoremprovingtostoreasequenceoflemmasintroducedbyauserto directtheproofsystemtowardssomefinaltheorem.Tablesofliterals canbeincorporatedintosequentcalculusproofsusingtwoideas.First, cutsareusedtoincorporatetableditemsintoaproof:onepremiseofthe cutrequiresaproofofthelemmaandtheotherbranchofthecutinserts thelemmaintothesetofassumptions.Second,toensurethatlemmais notreproved,weexploitthefactthatinfocusedproofs,atomscanhave differentpolarity.Usingtheseideas,simplelogicenginesthatdofocused proofsearch(suchaslogicprogramminginterpreters)areabletocheck proofsforcorrectnesswithguaranteesthatpreviousworkisnotredone. Wealsodiscusshowatablecanbeseenasaproofobjectanddiscuss somepossibleusesoftables-as-proofs. 1Introduction Asequenceofwellchosenlemmasisoftenanimportantpartofpresentinga proofin,atleast,informalmathematics.Insomesituations,onemightfeelthat thesequenceoflemmasitselfcouldconstituteanactualproof,particularlyifthe readeroftheproofhassignificantmathematicalmeanstofillinthegapsbetween thelemmas.Ofcourse,aslemmasatthebeginningofthelistareproved,they canbeusedtohelpprovelemmaslaterinthelist. Althoughgeneratinglemmasisawellknownandcriticalactivityinmathe- maticalproof,producingandusingsuchlemmascanbeimportantin,say,logic programming,deductivedatabases,andmodelchecking.Insuchsettings,the underlyingproofsthatsuchsystemsattempttobuildareusuallycut-free(that is,theylacktheuseoflemmas).Thatdoesnotmean,however,thatlemmas (and,hence,thecut-inferencerule)donothavearoleinimprovingthesearch fororthepresentationofproofs. Considerattemptingtoprovetheconjunctivequery B ∧ C fromalogicpro- gram Γ .Thisattemptcanbereducedtofirstattemptingtoprove B from Γ and then C from Γ .Itmightwellbethecasethatduringtheattempttoprove C ,