A formally verified prover for the ALC description logic (in PVS)

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: 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. 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 Version PVS-3.2. Version PVS-4.2. Version PVS-5.0.
Documentation:	Papers and reports related with this work: A formally verified prover for the ALC description logic. Constructing Formally Verified Reasoners for the ALC Description Logic. Formalización de la lógica descriptiva ALC en PVS.