Diferencia entre revisiones de «A formally verified prover for the ALC description logic in PVS»
| Línea 10: | Línea 10: | ||
|- | |- | ||
| '''Description:''' | | '''Description:''' | ||
| − | | | + | | The developed work consist of two phases: |
| − | + | # 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. | |
| + | # 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:57 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: | The developed work consist of two phases:
|
| Code: | You can find the PVS theories in ... |
| Documentation: | Proving termination with multiset orderings in PVS: theory, methodology and applications |
