Diferencia entre revisiones de «Verification of the formal concept analysis in PVS»
Línea 1: | Línea 1: | ||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
{| border="1" | {| border="1" | ||
| '''Title:''' | | '''Title:''' | ||
− | | | + | | Verification of the formal concept analysis in PVS |
|- | |- | ||
| '''Authors:''' | | '''Authors:''' | ||
− | | {{jalonso}}, {{mjoseh}} and {{ | + | | {{jalonso}}, {{mjoseh}}, {{fmartin}} and {{jruiz}}. |
|- | |- | ||
| '''Date:''' | | '''Date:''' | ||
− | | | + | | 2002-2004. |
|- | |- | ||
| '''Description:''' | | '''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:''' | | '''Code:''' |
Revisión del 11:11 2 jun 2010
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 in ... |
Documentation: | Proving termination with multiset orderings in PVS: theory, methodology and applications |