Isabelle HOL and SMT

-

English
73 Pages
Read an excerpt
Gain access to the library to view online
Learn more

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


Subjects

Informations

Published by
Reads 7
Language English
Report a problem
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 ofVand =andreflexivity, 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