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

De WikiGLC
Saltar a: navegación, buscar
Línea 7: Línea 7:
 
|-
 
|-
 
| '''Date:'''  
 
| '''Date:'''  
|  
+
| 2005-2007
 
|-
 
|-
 
| '''Description:'''  
 
| '''Description:'''  
|  
+
| * First part: 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. 
 +
* Second part: 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:'''  
 
| '''Code:'''  

Revisión del 10:55 2 jun 2010

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: * First part: 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.
  • Second part: 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: Proving termination with multiset orderings in PVS: theory, methodology and applications