Isabelle HOL and SMT

Sascha Böhme

Description

Niveau: Supérieur
Isabelle/HOL and SMT Sascha Bohme Technische Universitat Munchen September 10, 2009

• higher-order resolution


• theories proof


• smt


• intuitionistic higher-order


• isabelle's meta-logic


• outline introduction

Informations

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

Extrait

Isabelle/HOL and SMT

SaschaBo¨hme

TechnischeUniversita¨tMu¨nchen

September 10, 2009

Outline

1

2

3

4

Introduction

From Isabelle/HOL to SMT ...

Introduction Isabelle/HOL SMT Isabelle/HOL and SMT

From Isabelle/HOL to SMT ... Supported SMT Solvers Preprocessing

... and back again Z3 Proofs Proof Reconstruction for Z3 Evaluation

Conclusion

... and back again

Conclusion

2

Outline

Introduction

From Isabelle/HOL to SMT ...

Isabelle – A Generic Theorem Prover

Kernel

Infra- structure

... and back again

theorems: abstract type inference rules: intuitionistic higher-order logic

terms, types, . . .

Conclusion

3

Outline

Introduction

Isabelle – A Generic

theories

From Isabelle/HOL to SMT ...

Theorem Prover

proof tools

object logic

Kernel

Infra- structure

... and back again

theorems: abstract type inference rules: intuitionistic higher-order logic

terms, types, . . .

Conclusion

3

Outline

Introduction

From Isabelle/HOL to SMT ...

Isabelle’s Meta-Logic

Terms: constants ( V , =⇒,≡) variables λ-abstraction

application

Theorems:H`P

... and back again Conclusion

Rules: assumption introduction and elimination of V and =⇒and≡ reflexivity, symmetry, transitivity, congruence generalization, instantiation higher-order resolution

4

Outline

Introduction

From Isabelle/HOL to SMT ...

... and back again

Isabelle/HOL – Higher-Order Logic in Isabelle

theories

proof tools

object logic

Kernel

Infra- structure

theorems: abstract type inference rules: intuitionistic higher-order logic

terms, types, . . .

Conclusion

5

Outline

Introduction

From Isabelle/HOL to SMT ...

... and back again

Isabelle/HOL – Higher-Order Logic in Isabelle

theories

HOL

proof tools

Kernel

Infra- structure

Conclusion

shallow embedding in meta logic usual connectives and functions

theorems: abstract type inference rules: intuitionistic higher-order logic

terms, types, . . .

5