@MISC\{IMM2011-06046,
    author       = "I. Faizi",
    title        = "A Description Logic Prover in Prolog",
    year         = "2011",
    publisher    = "Technical University of Denmark, {DTU} Informatics, {E-}mail: reception@imm.dtu.dk",
    address      = "Asmussens Alle, Building 305, {DK-}2800 Kgs. Lyngby, Denmark",
    note         = "Supervised by Associate Professor J{\o}rgen Villadsen, jv@imm.dtu.dk, {DTU} Informatics",
    url          = "http://www.imm.dtu.dk/English.aspx",
    abstract     = "This work presents development of educational resources for teaching Description Logics and reasoning about them using Tableaux algorithms. The starting point of this work is the Master thesis of Thomas Herchenroder from the University of Edinburgh. Using Herchenroder's work and his implementation of Tableaux algorithm for reasoning in {ALC} , two extensions are developed. One of these extensions introduces an alternative ontology format that is more human-friendly compared to the one used by Herchenroder. In addition, a converter is developed that converts expressions between the two formats. The second extension, Xtableaux.pl, is directly developed on top of the Prolog implementation of Herchenroder, tableaux.pl. This extension is meant to construct the intermediate steps in the proof process. The intention behind this extension is to help students understand the Tableaux algorithms and help in debugging the ontology."
}