The Veblen hierarchy is an extension of the construction of epsilon numbers (fixpoints of the exponential map: ωε = ε). It is a collection φα of the Veblen Functions where φ0(β) = ωβ and φ1(β) = εβ. The sequence of fixpoints of φ1 function form φ2, etc. For a limit non empty ordinal λ the function φλ is the sequence of common fixpoints of all functions φα where α < λ.The Mizar formalization of the concept cannot be done directly as the Veblen functions are classes (not (small) sets). It is done...

This paper is concerned with a formal verification of the Formal Concept Analysis framework. We use the PVS system to represent and formally verify some algorithms of this theory. We also develop a method to transform specifications of algorithms based on finite sets into other executable ones, preserving its correctness. We illustrate this method by constructing an executable algorithm to compute an implicational base of the system of implications between attributes of a finite formal context.