Verification of the formal concept analysis in PVS

De WikiGLC
Revisión del 12:15 4 oct 2011 de Mjoseh (discusión | contribuciones)
(dif) ← Revisión anterior | Revisión actual (dif) | Revisión siguiente → (dif)
Saltar a: navegación, buscar
Title: Verification of the formal concept analysis in PVS
Authors: José A. Alonso, María J. Hidalgo, Francisco J. Martín and José L. Ruiz Reina.
Date: 2002-2004.
Description: This theory consists of a formal verification of the mathematical foundations of theory of the Formal Concept Analysis (FCA) framework in the PVS system. The notion of formal concept in a formal context is defined and we prove that the concepts of a context can be interpreted as a complete lattice. We also deal with the implications between attributes and we verify an algorithm to obtain a minimal base of implications. Finally, we transform the previous specifications of FCA into their respective executable specifications by using refinements, in order to preserve their properties.
Code: You can find the PVS theories
Documentation: Papers and documents related with this work: