| 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:
- 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:
|
You can find the PVS theories in
|
| Documentation:
|
Papers and reports related with this work:
|
