A formally verified prover for the ALC description logic (or Constructing formally verified reasoners for the ALC description logic)

De WikiGLC
Saltar a: navegación, buscar
  • Title: A formally verified prover for the ALC description logic.
  • 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:
Obtenido de «https://www.glc.us.es/web/index.php?title=A_formally_verified_prover_for_the_ALC_description_logic_(or_Constructing_formally_verified_reasoners_for_the_ALC_description_logic)&oldid=890»