A formally verified prover for the ALC description logic in PVS
Revisión del 10:55 2 jun 2010 de Mjoseh (discusión | contribuciones)
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: | * 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.
|
Code: | You can find the PVS theories in ... |
Documentation: | Proving termination with multiset orderings in PVS: theory, methodology and applications |