A proof theoretical journey through programming model checking and

pages

English

Documents

Écrit par
David Baelde

Publié par
chaeh

Lire un extrait

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

Découvre YouScribe et accède à tout notre catalogue !

Je m'inscris

Découvre YouScribe et accède à tout notre catalogue !

Je m'inscris

pages

English

Documents

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
A proof-theoretical journey through programming, model checking and theorem proving David Baelde IT University of Copenhagen ASL Meeting, Structural Proof Theory Session Madison, Wisconsin, April 2012 1 / 26

messy sequent

structural proof

logic programming

theory session

focused proofs

proof-theoretical journey

Voir

Publié par

chaeh

Langue

English

Philippus Baldaeus Logic programming

Aproof-theoreticaljourneythroughprogramming,modelcheckingandtheoremprovingDavidBaeldeITUniversityofCopenhagenASLMeeting,StructuralProofTheorySessionMadison,Wisconsin,April20121/62

oLigcrpgoarmmnigAspeciﬁcation(Γ)∀k.appnilkk∀x∀l∀k∀m.applkm⊃app(x::l)k(x::m)Messysequentcalculusproofs...Γ,∀k∀m.app[4]km⊃app[3;4]k(3::m)`app[0]nil[0]Γ`app[0]nil[0]Γ,appnil[1;2;3][1;2;3]`app[0]nil[0]Γ`app[0]nil[0]2/62

Voir