TY  - BOOK
AU  - Rademaker,Alexandre
ED  - SpringerLink (Online service)
TI  - A Proof Theory for Description Logics
T2  - SpringerBriefs in Computer Science,
SN  - 9781447140023
AV  - QA8.9-QA10.3 
U1  - 005.131 23
PY  - 2012///
CY  - London
PB  - Springer London, Imprint: Springer
KW  - Computer science
KW  - Computer Science
KW  - Mathematical Logic and Formal Languages
KW  - Mathematics of Computing
N1  - Introduction -- Background -- Sequent Calculus for ALC -- Comparing SCalc with other ALC Deduction Systems -- Natural Deduction for ALC.- A Proof Theory for ALCQI -- Proofs and Explanations -- A Prototype Theorem Prover -- Conclusion
N2  - 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
UR  - http://dx.doi.org/10.1007/978-1-4471-4002-3
ER  -