@book(Baader:1,
 editor       = {F. Baader and D. Calvanese and D. L. McGuinness and D. Nardi and Patel{-}Schneider, P. F.},
 year         = {2003},
 title        = {The Description Logic Handbook: Theory, Implementation, and Applications},
 publisher    = {Cambridge University Press},
)
@incollection(Baader:2,
 author       = {F. Baader and I. Horrocks and U. Sattler},
 year         = {2008},
 title        = {Description Logics},
 booktitle    = {Handbook of Knowledge Representation},
 series       = {Foundations of Artificial Intelligence},
 volume       = {3},
 publisher    = {Elsevier},
 pages        = {135--179},
 doi          = {10.1016/S1574-6526(07)03003-9},
)
@book(Bibel:2,
 author       = {W. Bibel},
 year         = {1993},
 title        = {Deduction - automated logic},
 publisher    = {Academic Press},
)
@inproceedings(Borgida:1,
 author       = {A. Borgida and E. Franconi and I. Horrocks},
 year         = {2000},
 title        = {Explaining $\mathcal{ALC}$ Subsumption},
 booktitle    = {{ECAI} 2000, Proceedings of the 14th European Conference on Artificial Intelligence, Berlin, Germany, 2000},
 pages        = {209--213},
)
@inproceedings(Freitas:1,
 author       = {F. Freitas and J. Otten},
 year         = {2016},
 title        = {A Connection Calculus for the Description Logic $\mathcal{ALC}$},
 booktitle    = {Advances in Artificial Intelligence - 29th Canadian Conference on Artificial Intelligence, Canadian {AI} 2016, Victoria, BC, Canada, May 31 - June 3, 2016. Proceedings},
 pages        = {243--256},
 doi          = {10.1007/978-3-319-34111-8\_30},
)
@book(Girard:1,
 author       = {Jean-Yves Girard and Paul Taylor and Yves Lafont},
 year         = {1989},
 title        = {{Proofs and Types}},
 publisher    = {Cambridge University Press},
)
@article(Horrocks:1,
 author       = {I. Horrocks},
 year         = {2008},
 title        = {Ontologies and the semantic web},
 journal      = {Commun. {ACM}},
 volume       = {51},
 number       = {12},
 pages        = {58--67},
 doi          = {10.1145/1409360.1409377},
)
@inproceedings(Melo:1,
 author       = {D. Melo and F. Freitas and J. Otten},
 year         = {2017},
 title        = {{RACCOON:} {A} Connection Reasoner for the Description Logic {ALC}},
 booktitle    = {LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017},
 pages        = {200--211},
)
@inproceedings(Otten:1,
 author       = {J. Otten},
 year         = {2011},
 title        = {A Non-clausal Connection Calculus},
 booktitle    = {Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, {TABLEAUX} 2011, Bern, Switzerland, July 4-8, 2011. Proceedings},
 pages        = {226--241},
 doi          = {10.1007/978-3-642-22119-4\_18},
)
@phdthesis(Palmeira:2,
 author       = {E. Palmeira},
 year         = {2017},
 title        = {Conversion of Proof in Description Logic $\mathcal{ALC}$ Generated by Connection Method into Sequents},
 school       = {Federal University of Pernambuco},
)
@article(Plaisted:1,
 author       = {D. A. Plaisted and S. Greenbaum},
 year         = {1986},
 title        = {A Structure-Preserving Clause Form Translation},
 journal      = {J. Symb. Comput.},
 volume       = {2},
 number       = {3},
 pages        = {293--304},
 doi          = {10.1016/S0747-7171(86)80028-1},
)