Focused Inductive Theorem Proving
15 pages
English

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Focused Inductive Theorem Proving

-

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
15 pages
English
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Niveau: Supérieur, Doctorat, Bac+8
Focused Inductive Theorem Proving David Baelde1, Dale Miller2, and Zachary Snow1 1 Digital Technology Center and Dept of CS, University of Minnesota 2 INRIA & LIX, Ecole Polytechnique Abstract. Focused proof systems provide means for reducing and struc- turing the non-determinism involved in searching for sequent calculus proofs. We present a focused proof system for a first-order logic with in- ductive and co-inductive definitions in which the introduction rules are partitioned into an asynchronous phase and a synchronous phase. These focused proofs allow us to naturally see proof search as being organized around interleaving intervals of computation and more general deduc- tion. For example, entire Prolog-like computations can be captured us- ing a single synchronous phase and many model-checking queries can be captured using an asynchronous phase followed by a synchronous phase. Leveraging these ideas, we have developed an interactive proof assistant, called Tac, for this logic. We describe its high-level design and illustrate how it is capable of automatically proving many theorems using induc- tion and coinduction. Since the automatic proof procedure is structured using focused proofs, its behavior is often rather easy to anticipate and modify. We illustrate the strength of Tac with several examples of proved theorems, some achieved entirely automatically and others achieved with user guidance. 1 Introduction The sequent calculus of Gentzen is a well-studied proof framework used to de- scribe provability for a number of logics.

  • logic

  • fixed point

  • usual small step

  • focused proof

  • proof systems

  • introduction rules

  • using µ

  • sx bsx


Sujets

Informations

Publié par
Nombre de lectures 9
Langue English

Extrait

FocusedInductiveTheoremProvingDavidBaelde1,DaleMiller2,andZacharySnow11DigitalTechnologyCenterandDeptofCS,UniversityofMinnesota2INRIA&LIX,E´colePolytechniqueAbstract.Focusedproofsystemsprovidemeansforreducingandstruc-turingthenon-determinisminvolvedinsearchingforsequentcalculusproofs.Wepresentafocusedproofsystemforafirst-orderlogicwithin-ductiveandco-inductivedefinitionsinwhichtheintroductionrulesarepartitionedintoanasynchronousphaseandasynchronousphase.Thesefocusedproofsallowustonaturallyseeproofsearchasbeingorganizedaroundinterleavingintervalsofcomputationandmoregeneraldeduc-tion.Forexample,entireProlog-likecomputationscanbecapturedus-ingasinglesynchronousphaseandmanymodel-checkingqueriescanbecapturedusinganasynchronousphasefollowedbyasynchronousphase.Leveragingtheseideas,wehavedevelopedaninteractiveproofassistant,calledTac,forthislogic.Wedescribeitshigh-leveldesignandillustratehowitiscapableofautomaticallyprovingmanytheoremsusinginduc-tionandcoinduction.Sincetheautomaticproofprocedureisstructuredusingfocusedproofs,itsbehaviorisoftenrathereasytoanticipateandmodify.WeillustratethestrengthofTacwithseveralexamplesofprovedtheorems,someachievedentirelyautomaticallyandothersachievedwithuserguidance.1IntroductionThesequentcalculusofGentzenisawell-studiedproofframeworkusedtode-scribeprovabilityforanumberoflogics.Thisframeworkalsoseemstobeanaturalsettingfororganizingthesearchforproofsinatheoremprover.Forex-ample,asequentoftheformΣ;Γ`BdenotestheobligationofshowingthattheformulaBfollowsfromtheassumptionsinthe(multi)setΓforeveryinstan-tiationofthevariablesinΣ.Anattempttoproveaformula,sayB0,thengivesrisetoattemptstoapplyinferencerulesrepeatedlytotherootsequent;∙`B0leaving,atsomepoint,openpremisesΣ1;Γ1`B1,...,Σn;Γn`Bn.Thissetofsequentsrepresentsonewaytodecomposetheoriginalproofobligationinton0subgoals.Thefrontieroftheopenprooftreecanrepresenttheabstractstateofanidealizedtheoremprover.Thesequentcalculusis,unfortunately,fartoonon-deterministictodirectlyorganizeatheoremprover.Forexample,considerthecasewhenthereareevenjusttwohypothesesonwhichtowork.Thesequentcalculusdoesnotspecifyonwhichtoworkfirst,andsoonemightfirstworkonone,thentheother,alternatingbackandforth.Thiscreatesanexplosivenumberofalternatives
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • Podcasts Podcasts
  • BD BD
  • Documents Documents