On the proof theory of ALC

MaRDI QIDQ3086706zbMATH OpenFDO

Authors

Publication date 30 March 2011

zbMATH Keywords

computational content of proofscut eliminationdescription logicsequent calculus

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Logic in artificial intelligence (68T27) Knowledge representation (68T30)

Recommendations

• A proof theory for description logics.
• An overview of tableau algorithms for description logics
• A connection calculus for the description logic \( {\mathcal{ALC}} \)
• \({\mathcal KALC}\): a constructive semantics for \({\mathcal ALC}\)
• ABox abduction in the description logic \(\mathcal{ALC}\)

Cited in

(4)

• scientific article; zbMATH DE number 1696553 (Why is no real title available?)
• A connection calculus for the description logic \( {\mathcal{ALC}} \)
• A proof theory for description logics.
• On the proof theory of Coquand's calculus of constructions

This page was built for publication: On the proof theory of \({\mathcal{ALC}}\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3086706)