Supraconfianza lógica en la Web Semántica

Este post trata directamente sobre el tema de investigación del grupo al que pertenezco, dentro del marco del proyecto TIN titulado: Sistemas verificados para el razonamiento en la Web Semántica. El objetivo: construir demostradores automáticos formalmente verificados para razonar con ontologías. Es decir, completar la confianza objetivo de la Web Semántica con la supraconfianza lógica, es decir, los propios razonadores son fiables (están verificados). Dificultades: no existe nada parecido, sólo algunas especificaciones sobre ACL2 y PVS pero no son completas. He participado modestamente en el diseño de la especificación en PVS de la primera lógica descriptiva utilizada, ALC. Cuando decimos esto, nos referimos que la sintaxis, semántica y un primer algoritmo (basado en tableros) han sido implementado y verificado en PVS. Esta ingente y compleja tarea ha sido llevada a cabo por M.J. Hidalgo y J.A. Alonso. Nos han aceptado un trabajo en el TPHOLS 2007 donde se describe la especificación (A formally verified prover for the ALC description logic), y se prepara otro donde se describe cómo de la especificación (que en definitiva es un marco genérico) se deduce de manera directa la verificación de algoritmos concretos. El reto será comprobar cuánto de extensible tiene ese marco, para acercarse a lógicas descriptivas más expresivas, así como a demostradores automáticos optimizados. La tarea es muy interesante: una lógica como la de PVS debe ser capaz de interpretar muchas lógicas descriptivas, pero la tarea de desarrollo de la teoría correspondiente será muy ardua.

Anuncios