SAT-based finite model generation for higher-order logic [Elektronische Ressource] / Tjark Weber

Tjark Weber

Description

ff f ff f f ff ff f ff f f ff f fSAT-based Finite Model Generationfor Higher-Order LogicTjark WeberLehrstuhl fur Software & Systems EngineeringInstitut fur InformatikTechnische Universitat MunchenLehrstuhl fur Software & Systems EngineeringInstitut fur InformatikTechnische Universitat Munchen SAT-based Finite Model Generationfor Higher-Order LogicTjark WeberVollstandiger Abdruck der von der Fakultat fur Informatik der Technischen Universitat Munc henzur Erlangung des akademischen Grades einesDoktors der Naturwissenschaften (Dr. rer. nat.)genehmigten Dissertation.Vorsitzender: Univ.-Prof. F. J. Esparza EstaunPrufer der Dissertation: 1. Univ.-Prof. T. Nipkow, Ph. D.2. Univ.-Prof. Dr. H. Veith, Technische Universitat DarmstadtDie Dissertation wurde am 30. April 2008 bei der Technischen Universitat Munchen eingereicht und durch die Fakultat fur Informatik am 30. September 2008 angenommen.KurzfassungDiese Arbeit prasen tiert zwei Erweiterungen des Theorembeweisers Isabelle/HOL, einem aufLogik hoherer Stufe basierenden System.Der Hauptbeitrag ist ein Modellgenerator fur hoherstu ge Logik, der seine Eingabeformel inAussagenlogik ubersetzt, so dass ein herkommlicher SAT-Solver fur die eigentliche Modellsuche verwendet werden kann. Die Korrektheit der Ubersetzung wird gezeigt.

Sujets

• Informatik
• Mathematics

Informations

• Publié par: technische_universitat_munchen
• Publié le: 01 janvier 2008
• Nombre de lectures: 20
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

❢

❢

❢❢❢

❢

❢❢❢❢

SAT-basedFiniteModelGeneration

rfo

LogicHigher-Order

❢

❢❢❢❢

❢

❢❢❢❢

rkTja

erebW

Lehrstuhlf¨urSoftware&SystemsEngineering
Institutf¨urInformatik
TechnischeUniversit¨atM¨unchen

Lehrstuhlf¨urSoftware&SystemsEngineering
Institutf¨urInformatik
TechnischeUniversit¨atM¨unchen

SAT-basedFiniteModelGeneration
LogicHigher-Orderrfo

erebWrkTja

Vollst¨andigerAbdruckdervonderFakult¨atf¨urInformatikderTechnischenUniversit¨atM¨unchen
zurErlangungdesakademischenGradeseines
DoktorsderNaturwissenschaften(Dr.rer.nat.)
Dissertation.genehmigten

Vorsitzender:Univ.-Prof.F.J.EsparzaEstaun

Pr¨uferderDissertation:1.Univ.-Prof.T.Nipkow,Ph.D.

2.Univ.-Prof.Dr.H.Veith,TechnischeUniversit¨atDarmstadt

DieDissertationwurdeam30.April2008beiderTechnischenUniversit¨atM¨uncheneingereicht
unddurchdieFakult¨atf¨urInformatikam30.September2008angenommen.

Kurzfassung

DieseArbeitpr¨asentiertzweiErweiterungendesTheorembeweisersIsabelle/HOL,einemauf
Logikh¨ohererStufebasierendenSystem.

DerHauptbeitragisteinModellgeneratorf¨urh¨oherstufigeLogik,derseineEingabeformelin
Aussagenlogik¨ubersetzt,sodasseinherk¨ommlicherSAT-Solverf¨urdieeigentlicheModellsuche
verwendetwerdenkann.DieKorrektheitder¨Ubersetzungwirdgezeigt.DerModellgeneratorist
indasIsabelle-Systemintegriertworden,unterst¨utztverschiedenedefinitorischeMechanismen,
wiesieinIsabelle/HOLzurVerf¨ugungstehen,undistaufmehrereFallstudienangewandt
orden.w

Darlogisc¨ubheerThinausautologiensindk¨SAonnenT-SolvvonerbeinemewSAeisgenerierendT-SolverbmitewiesIsabenwelleinerden,tegriertundwdervorden:ondemAussagen-Solver
ProblemsgefundeneerlaubtResolutionsbdieVewerifieiskationwirdvvononBewIsabeisenellevmiterifiziert.mehrerenEineg¨MillionenunstigeReprResolutionssc¨asentationhrittedesn.

i

ii

Abstract

ThisthesispresentstwoextensionstothetheoremproverIsabelle/HOL,alogicalframework
logic.higher-orderonbased

Themaincontributionisamodelgeneratorforhigher-orderlogicthatproceedsbytranslating
theinputformulatopropositionallogic,sothatastandardSATsolvercanbeemployedfor
theactualmodelsearch.Thetranslationisprovedcorrect.Themodelgeneratorhasbeen
integratedwiththeIsabellesystem,extendedtosupportsomeofthedefinitionalmechanisms
providedbyIsabelle/HOL,andappliedtovariouscasestudies.

Moreositionalver,SAtautologiesTsolvcanersbhaevperobveenedbinyategratedSATsolvwither,Isabandelletheinaresolutionproof-proproofducingfoundbfashion:ythepropsolvo-er
isverifiedbyIsabelle.Anadequaterepresentationoftheproblemallowstoverifyproofswith
steps.resolutionofmillions

iii

iv

tswledgemenknoAc

IwouldliketothankTobiasNipkow,mysupervisor,forhisinvaluablesupport,advice,and
patience.Thecurrentandformermembersofhisresearchgrouphavecontributedtoafruitful
workenvironment:ClemensBallarin,GertrudBauer,StefanBerghofer,AmineChaieb,Florian
Haftmann,GerwinKlein,FarhadMehta,StevenObua,NorbertSchirmer,SebastianSkalberg,
MartinStrecker,MarkusWenzel,andMartinWildmoser.IamparticularlyindebtedtoLars
EbertandMarcoHelmersforproof-readingmythesis,toMichaelFortleffforprovidingshelter,
andtoNorafordistractingme.IthankHelmutVeithforactingasareferee.
MythanksalsogotoHelmutSchwichtenberg,speakerofthe“GraduiertenkollegLogikinder
Informatik”,whichprovidedbothfinancialandintellectualsupport,andtotheothermembers
oftheGraduiertenkolleg—inparticulartoAndreasAbel,KlausAehlig,SteffenJost,andRalph
Matthesforinspiringdiscussionsandmore.
Manyotherpeoplehaveinfluencedthisthesisinonewayoranother.AmongthemareReinhold
Letz,GernotStenz,JanJ¨urjens,andManfredBroyfromTechnischeUniversit¨atM¨unchen,
MartinHofmannfromLudwig-Maximilians-Universit¨atM¨unchen,HasanAmjadandLarry
PaulsonfromtheUniversityofCambridge,SharadMalikandZhaohuiFufromPrincetonUni-
versity,PascalFontaine,StephanMerz,andAlwenTiufromINRIALorraine,JohnHarrison
fromIntelCorporation,JohnMatthewsfromGalois,Inc.,DavidAspinallfromtheUniver-
sityofEdinburgh,AnnabelleMcIverfromMacquarieUniversity,andMosheVardifromRice
.yersitUnivFinallyIwouldliketothankeveryonewhohasplayedapartinmakingthepastyearsin
Munichapleasantandsuccessfultimeforme.Friendsandfamilyhavebeenasteadysource
t.encouragemenof

v

vi

tstenCon

ductiontroIn11.1Motivation......................................
1.2Contributions.....................................
1.3RelatedWork.....................................
1.4Isabelle........................................
1.5Overview.......................................

GenerationdelMoFinite22.1Introduction......................................
2.2Higher-OrderLogic..................................
2.2.1Types.....................................
2.2.2Terms.....................................
2.2.3Satisfiability.................................
2.3TranslationtoPropositionalLogic.........................
2.3.1PropositionalLogic..............................
2.3.2InterpretationofTypes...........................
2.3.3InterpretationofTerms...........................
2.3.4Examples...................................
2.4ModelGeneration..................................
2.4.1FindingaSatisfyingAssignment......................
2.4.2TypeEnvironmentsandTypeModels...................
2.4.3TheAlgorithm................................
2.4.4BuildingtheHOLModel..........................
2.5Conclusion......................................

3ExtensionsandOptimizations
3.1Introduction......................................

vii

112346

778811141515162240414142434545

4747

viii

CONTENTS

3.2Optimizations.....................................48
3.3Isabelle’sMeta-Logic.................................52
3.4TypeandConstantDefinitions,Overloading....................52
3.4.1TypeDefinitions...............................52
3.4.2ConstantDefinitionsandOverloading...................53
3.4.3DefiniteDescriptionandHilbert’sChoice.................54
3.5AxiomaticTypeClasses...............................55
3.6DatatypesandRecursiveFunctions.........................56
3.6.1Non-RecursiveDatatypes..........................57
3.6.2RecursiveDatatypes.............................58
3.6.3RecursiveFunctions.............................64
3.7SetsandRecords...................................67
3.8HOLCF........................................68
3.9Conclusion......................................69

71StudiesCase44.1Introduction......................................71
4.2TheRSA-PSSSecurityProtocol..........................72
4.2.1AbstractProtocolFormalization......................72
4.2.2AvoidingConfusion.............................75
4.3ProbabilisticPrograms................................77
4.3.1TheProbabilisticModelLS.........................78
4.3.2TheAbstractModelKS...........................86
4.3.3MechanizationofCounterexampleSearch.................93
4.4ASAT-basedSudokuSolver.............................94
4.4.1ImplementationinIsabelle/HOL......................95
4.4.2TranslationtoPropositionalLogic.....................96
4.5Conclusion......................................98

5IntegrationofProof-producingSATSolvers99
5.1Introduction......................................99
5.2RelatedWork.....................................100
5.3SystemDescription..................................101
5.3.1Preprocessing.................................101
5.3.2ProofReconstruction.............................103

CONTENTS6

tationsRepresenClause5.3.3

5.4Evaluation............

5.5PersistentTheorems......

5.6Conclusion...........

Conclusion

6.1

6.2

Summary............

orkWutureF

..........

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

ix

110

112

115

117

119

119

120

x

CONTENTS

1Chapter

ductiontroIn

ationMotiv1.1

Allmenbynaturedesiretoknow.
B.C.350Aristotle,

Interactivetheoremprovingisaboutidentifyingfalseconjecturesalmostasmuchasitisabout
findingproofsfortheorems.Falseconjectu