A formally verified prover for the ALC description logic (or Constructing formally verified reasoners for the ALC description logic)
Revisión del 19:37 1 jun 2010 de Mjoseh (discusión | contribuciones)
- Title:
- Autores: José A. Alonso y María J. Hidalgo.
- Fecha de realización: 2002-2004.
- Abstract:
- 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:
