Ver el código de «Verification of the formal concept analysis in PVS»

{| border="1"
| '''Title:''' 
| Verification of the formal concept analysis in PVS
|-
| '''Authors:''' 
| {{jalonso}}, {{mjoseh}}, {{fmartin}} and {{jruiz}}.
|-
| '''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 [[Theory of Refinements in PVS|refinements]], in order to preserve their properties.
|-
| '''Code:''' 
| You can find the PVS theories
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-3.2/afc.tgz Version PVS-3.2].
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-4.2/afc.tgz Version PVS-4.2].
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-5.0/afc.tgz Version PVS-5.0].
|-
| '''Documentation:'''
| Papers and documents related with this work:
* [http://www.cs.us.es/~jalonso/trabajos_dirigidos/2004-tesis-MJHD.pdf Teoría computacional (en PVS) de la programación lógica y del análisis formal de conceptos (Tesis, Universidad de Sevilla, 2004)].
* [http://www.cs.us.es/~jalonso/publicaciones/2004-racsam.pdf Verification of the formal concept analysis].
|}