Formal verification of a proof procedure for the description logic ALC

Description Logics (DLs) are a family of languages used for the representation and reasoning on the knowledge of an application domain, in a structured and formal manner. In order to achieve this objective, several provers, such as RACER and FaCT++, have been implemented, but these provers themselve...

Full description

Bibliographic Details
Main Authors: Martin Strecker, Mohamed Mezghiche, Mohamed Chaabani
Format: Article
Language:English
Published: Open Publishing Association 2013-07-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1307.8211v1