Formalizaciones en PVS y el problema de las versiones

En la wiki del Grupo de Lógica Computacional se han publicados las formalizaciones en PVS 4.2 de las siguientes teorías:

• A Formalization of Abstract Properties of Confluent Reductions in PVS.
• Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO).
• A formally verified prover for the ALC description logic (in PVS).
• Verification of the formal concept analysis in PVS.
• A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution.
• Theory of Refinements in PVS.

La adaptación la ha realizado María J. Hidalgo a partir de la versión de PVS 3.2. El proceso de adaptación ha sido complejo por las diferencias existentes entre ambas versiones de PVS. Los principales problemas que han aparecido son los siguientes:

• Diferencia en el tratamiento de los juicios entre teorías situadas en distintos directorios y cargadas como extensiones del preludio.
• Diferencia en las opciones por defecto en estrategias predefinidas.
• Diferencia en el número de obligaciones de pruebas generadas.

Además, el problema de la compatibilidad entre las distintas versiones de los sistemas de razonamiento dificulta la reutilización de las teoría formalizadas. En concreto, en algunas teorías que hemos desarrollado se han usado teorías desarrolladas por otros como, por ejemplo, la teoría sobre puntos fijos de F. Bartels, A. Dold, F.W. v. Henke, H. Pfeifer y H. Rueß que está desarrollada en la versión 2.4 de PVS, no se ha adaptado a las siguientes versiones y no es adecuada para la versión actual de PVS.