A Proof Theory for Description Logics
Rademaker, Alexandre.
A Proof Theory for Description Logics [electronic resource] / by Alexandre Rademaker. - X, 106 p. 16 illus. online resource. - SpringerBriefs in Computer Science, 2191-5768 . - SpringerBriefs in Computer Science, .
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.
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.
9781447140023
10.1007/978-1-4471-4002-3 doi
Computer science.
Computer Science.
Mathematical Logic and Formal Languages.
Mathematics of Computing.
QA8.9-QA10.3
005.131
A Proof Theory for Description Logics [electronic resource] / by Alexandre Rademaker. - X, 106 p. 16 illus. online resource. - SpringerBriefs in Computer Science, 2191-5768 . - SpringerBriefs in Computer Science, .
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.
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.
9781447140023
10.1007/978-1-4471-4002-3 doi
Computer science.
Computer Science.
Mathematical Logic and Formal Languages.
Mathematics of Computing.
QA8.9-QA10.3
005.131