We compare alternative definitions of undirected graphical models for discrete, finite variables. Lauritzen [7] provides several definitions of such models and describes their relationships. He shows that the definitions agree only when joint distributions represented by the models are limited to strictly positive distributions. Heckerman et al. [6], in their paper on dependency networks, describe another definition of undirected graphical models for strictly positive distributions. They show that...

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.