A Proof Theory for Description Logics

2012. Auflage 2012
ISBN: 978-1-4471-4001-6
Verlag: Springer

Buch, Englisch, 106 Seiten, Format (B × H): 161 mm x 248 mm, Gewicht: 196 g

Reihe: SpringerBriefs in Computer Science

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.

Zielgruppe

Research

Autoren/Hrsg.

Rademaker, Alexandre

Fachgebiete

• Mathematik | Informatik EDV | Informatik Informatik Logik, formale Sprachen, Automaten
• Mathematik | Informatik EDV | Informatik Informatik Künstliche Intelligenz Wissensbasierte Systeme, Expertensysteme
• Mathematik | Informatik Mathematik Mathematik Allgemein Mathematische Logik

Inhaltsverzeichnis

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.