© 2012

A Proof Theory for Description Logics


Part of the SpringerBriefs in Computer Science book series (BRIEFSCOMPUTER)

Table of contents

  1. Front Matter
    Pages i-x
  2. Alexandre Rademaker
    Pages 1-7
  3. Alexandre Rademaker
    Pages 9-15
  4. Alexandre Rademaker
    Pages 17-36
  5. Alexandre Rademaker
    Pages 51-63
  6. Alexandre Rademaker
    Pages 65-75
  7. Alexandre Rademaker
    Pages 77-86
  8. Alexandre Rademaker
    Pages 87-102
  9. Alexandre Rademaker
    Pages 103-106

About this book


Description Logics (DLs) is a family of formalisms used to represent knowledge of a domain. They are equipped with a formal logic-based semantics. Knowledge representation systems based on description logics provide various inference capabilities that deduce implicit knowledge from the explicitly represented knowledge.

A Proof Theory for Description Logics introduces Sequent Calculi and Natural Deduction for some DLs (ALC, ALCQ). Cut-elimination and Normalization are proved for the calculi. The author argues that such systems can improve the extraction of computational content from DLs proofs for explanation purposes.


Description Logics Natural Deduction Proof Theory Sequent Calculus

Authors and affiliations

  1. 1.Applied Mathematics SchoolFundação Getúlio VargasRio de JaneiroBrazil

Bibliographic information

Industry Sectors
IT & Software