Diferencia entre revisiones de «A formally verified prover for the ALC description logic in PVS»

De WikiGLC
Saltar a: navegación, buscar
 
(No se muestran 4 ediciones intermedias de 2 usuarios)
Línea 15: Línea 15:
 
|-
 
|-
 
| '''Code:'''  
 
| '''Code:'''  
−
| You can find the PVS theories in ...
+
| You can find the PVS theories in
 +
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-3.2/alc.tgz Version PVS-3.2].
 +
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-4.2/alc.tgz Version PVS-4.2].
 +
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-5.0/alc.tgz Version PVS-5.0].
 +
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-5.0/alc_5.0_extension.tgz Version PVS-5.0 (extended)].
 
|-
 
|-
 
| '''Documentation:'''
 
| '''Documentation:'''
 
| Papers and reports related with this work:
 
| Papers and reports related with this work:
 
* [http://www.cs.us.es/~jalonso/publicaciones/2007-TPHOLs.pdf A formally verified prover for the ALC description logic].
 
* [http://www.cs.us.es/~jalonso/publicaciones/2007-TPHOLs.pdf A formally verified prover for the ALC description logic].
−
* [http://www.cs.us.es/~jalonso/publicaciones/2007-TPHOLs.pdf A formally verified prover for the ALC description logic].
+
* [http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4SKCGHV-6&_user=603129&_coverDate=05%2F23%2F2008&_rdoc=6&_fmt=high&_orig=browse&_srch=doc-info(%23toc%2313109%232008%23997999996%23690732%23FLP%23display%23Volume)&_cdi=13109&_sort=d&_docanchor=&_ct=11&_acct=C000031118&_version=1&_urlVersion=0&_userid=603129&md5=eec27556a50ac1058cd5ae61d55d1937 Constructing Formally Verified Reasoners for the ALC Description Logic].
−
* [http://www.cs.us.es/~jalonso/publicaciones/2007-TPHOLs.pdf A formally verified prover for the ALC description logic].
+
* [http://www.cs.us.es/~mjoseh/pub/Formalizacion_de_la_logica_descriptiva_ALC_en_PVS.pdf Formalización de la lógica descriptiva ALC en PVS].
 
|}
 
|}

Revisión actual del 12:21 7 jun 2012

Title: A formally verified prover for the ALC description logic.
Authors: José A. Alonso, María J. Hidalgo, Francisco J. Martín and José L. Ruiz Reina.
Date: 2005-2007
Description: The developed work consist of two phases:
  1. This theory is a PVS specification of a prover for the ALC description logic, as well as the proofs of its termination, soundness and completeness. We use the previous formalization of the well--foundedness of the multiset relation induced by a well--founded relation to prove the termination and the completeness of the ALC prover.
  2. In this theory we develop the construction of a formally verified generic tableau-based algorithm for checking satisfiability of ALC-concepts, from the previous generic framework. We do it using a methodology of refinements to transfer the properties from the framework to the algorithm. We also obtain some verified reasoners from the algorithm by a process of instantiation.
Code: You can find the PVS theories in
Documentation: Papers and reports related with this work:
Obtenido de «https://www.glc.us.es/web/index.php?title=A_formally_verified_prover_for_the_ALC_description_logic_in_PVS&oldid=1131»