### Abstract

This formalization includes a general framework for query optimization consisting of the definitions of selectivities, query graphs, join trees, and cost functions. Furthermore, it implements the join ordering algorithm IKKBZ using these definitions. It verifies the correctness of these definitions and proves that IKKBZ produces an optimal solution within a restricted solution space.

### License

BSD License

### Topics

- Computer science/Data management systems

### Session Query_Optimization

- Misc
- Graph_Theory_Batteries
- Graph_Definitions
- Shortest_Path_Tree
- Selectivities
- JoinTree
- CostFunctions
- Graph_Additions
- QueryGraph
- Directed_Tree_Additions
- Dtree
- List_Dtree
- IKKBZ
- IKKBZ_Optimality
- IKKBZ_Examples

### Depends on

- Graph Theory

## Cite

×

Query_Optimization-AFP

    @article{Query_Optimization-AFP,
      author  = {Lukas Stevens and Bernhard Stöckl},
      title   = {Verification of Query Optimization Algorithms},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Query_Optimization.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Oct 5, 2022 : Isabelle2021-1