A proof theoretical journey through programming model checking and

David Baelde

Description

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


• nil


• theory session


• focused proofs


• proof-theoretical journey


• app

Sujets

• Philippus Baldaeus
• Logic programming

Informations

• Publié par: chaeh
• Nombre de lectures: 32
• Langue: English

Extrait

Aproof-theoreticaljourneythrough programming,modelcheckingand theoremproving DavidBaelde ITUniversityofCopenhagen ASLMeeting,StructuralProofTheorySession Madison,Wisconsin,April2012 1/62

oLigcrpgoarmmnig Aspecification(Γ) ∀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