@book(dlhandbook,
 author       = "Franz Baader and Diego Calvanese and Deborah L. McGuinness and Daniele Nardi and Peter F. Patel-Schneider",
 year         = "2007",
 title        = "The Description Logic Handbook: Theory, Implementation, and Applications",
 publisher    = "Cambridge University Press",
 doi          = "10.1017/CBO9780511711787",
)
@inproceedings(Baader1991,
 author       = "Franz Baader and Philipp Hanschke",
 year         = "1991",
 title        = "A schema for integrating concrete domains into concept languages",
 booktitle    = "Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI'91)",
 pages        = "452--457",
)
@inproceedings(BaaderHS05,
 author       = "Franz Baader and Ian Horrocks and Ulrike Sattler",
 year         = "2005",
 title        = "Description Logics as Ontology Languages for the Semantic Web",
 booktitle    = "Mechanizing Mathematical Reasoning",
 pages        = "228--248",
 doi          = "10.1007/978-3-540-32254-2\_14",
 url          = "http://www.informatik.uni-trier.de/~ley/db/conf/birthday/siekmann2005.html#BaaderHS05",
)
@article(BaaderSattler-JLC-99,
 author       = "Franz Baader and Ulrike Sattler",
 year         = "1999",
 title        = "Expressive Number Restrictions in Description Logics",
 journal      = "Journal of Logic and Computation",
 volume       = "9",
 number       = "3",
 pages        = "319--350",
 doi          = "10.1093/logcom/9.3.319",
 url          = "http://lat.inf.tu-dresden.de/research/papers/1999/BaaderSattler-JLC-99.ps.gz",
)
@article(Baader00tableaualgorithms,
 author       = "Franz Baader and Ulrike Sattler",
 year         = "2001",
 title        = "An Overview of Tableau Algorithms for Description Logics",
 journal      = "Studia Logica",
 volume       = "69",
 number       = "1",
 pages        = "5--40",
 doi          = "10.1023/A:1013882326814",
 url          = "http://lat.inf.tu-dresden.de/research/papers/2001/BaaderSattler-StudiaLogica.ps.gz",
)
@inproceedings(Berardi01reasoningon,
 author       = "Daniela Berardi and Diego Calvanese and Guiseppe De Giacomo",
 year         = "2001",
 title        = "Reasoning on {UML} Class Diagrams using Description Logic Based Systems",
 booktitle    = "Proc of the KI 2001 Workshop on Applications of Description Logics, CEUR Electronic Workshop Proceedings, http://ceur-ws.org/Vol-44",
)
@inproceedings(chaabani09:_formal_de_la_logiq_descr,
 author       = "Mohamed Chaabani and Mohamed Mezghiche and Martin Strecker",
 year         = "2009",
 title        = "Formalisation de la logique de description $\mathcal {ALC}$ dans l'assistant de preuve {Coq}",
 editor       = "L. Bellatrache and G. Kassel and P. Thiran",
 booktitle    = "Proc. 3es Journ{\'e}es francophones sur les ontologies",
 pages        = "139--147",
)
@inproceedings(chaabani10_afadl,
 author       = "Mohamed Chaabani and Mohamed Mezghiche and Martin Strecker",
 year         = "2010",
 title        = "V{\'e}rification d'une m{\'e}thode de preuve pour la logique de description {$\cal {ALC}$}",
 booktitle    = "Proc. 10{\`e}me Journ{\'e}es Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels",
 pages        = "149--163",
)
@inproceedings(Fehreretal94a,
 author       = "Detlef Fehrer and Ullrich Hustadt and Manfred Jaeger and Andreas Nonnengart and Hans J{\"u}rgen Ohlbach and Renate A. Schmidt and Christoph Weidenbach and Emil Weydert",
 year         = "1994",
 title        = "Description Logics for Natural Language Processing",
 editor       = "Franz Baader and Maurizio Lenzerini and Werner Nutt and Peter F. Patel-Schneider",
 booktitle    = "International Workshop on Description Logics '94",
 series       = "Document",
 volume       = "D-94-10",
 publisher    = "DFKI",
 address      = "Bonn, Germany",
 pages        = "80--84",
)
@inproceedings(Racer,
 author       = "Volker Haarslev and Ralf M\"{o}ller",
 year         = "2001",
 title        = "RACER System Description",
 booktitle    = "IJCAR '01: Proc. First International Joint Conference on Automated Reasoning",
 publisher    = "Springer-Verlag",
 pages        = "701--706",
 doi          = "10.1007/3-540-45744-5\_59",
)
@inproceedings(hidalgo07:_alc,
 author       = "Mar{\'i}a-Jos{\'e} Hidalgo and Jos{\'e}-Antonio Alonso and Joaqu{\'i}n Borrego-D{\'i}az and Francisco-Jesus Martin-Mateos and Jos{\'e}-Luis Ruiz-Reina",
 year         = "2007",
 title        = "A formally verified prover for the ALC description logic.",
 booktitle    = "20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007",
 series       = "Lecture Notes in Computer Science",
 volume       = "4732",
 pages        = "135--150",
 doi          = "10.1007/978-3-540-74591-4\_11",
 url          = "http://www.cs.us.es/~mjoseh/pub/2007-TPHOLs.pdf",
)
@article(Horrocks,
 author       = "Ian Horrocks and Ulrike Sattler",
 year         = "2007",
 title        = "A Tableau Decision Procedure for $\mathcal {SHOIQ}$",
 journal      = "J.\ of Automated Reasoning",
 volume       = "39",
 number       = "3",
 pages        = "249--276",
 doi          = "10.1007/s10817-007-9079-9",
 url          = "download/2007/HoSa07a.pdf",
)
@inproceedings(luther09:_who_heck_father_bob,
 author       = "Marko Luther and Thorsten Liebig and Sebastian B{\"o}hm and Olaf Noppens",
 year         = "2009",
 title        = "{Who the Heck is the Father of Bob?}",
 booktitle    = "6th Annual European Semantic Web Conference (ESWC2009)",
 pages        = "66--80",
 url          = "http://data.semanticweb.org/conference/eswc/2009/paper/222",
)
@book(Isabelle_Tutorial,
 author       = "Tobias Nipkow and Lawrence Paulson and Markus Wenzel",
 year         = "2002",
 title        = "Isabelle/HOL. A Proof Assistant for Higher-Order Logic",
 series       = "Lecture Notes in Computer Science",
 volume       = "2283",
 publisher    = "Springer",
 doi          = "10.1007/3-540-45949-9",
)
@article(DBLP:conf/kr/DoniniLNN91,
 author       = "Werner Nutt and Francesco M. Donini and Maurizio Lenzerini and Daniele Nardi",
 year         = "1997",
 title        = "The complexity of concept languages",
 journal      = "Inf. Comput.",
 volume       = "134",
 number       = "1",
 pages        = "1--58",
 doi          = "10.1006/inco.1997.2625",
)
@inproceedings(ridge05:_fol,
 author       = "Tom Ridge and James Margetson",
 year         = "2005",
 title        = "A mechanically verified, sound and complete theorem prover for {FOL}",
 editor       = "Joe Hurd and Tom Melham",
 booktitle    = "18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005",
 series       = "Lecture Notes in Computer Science",
 volume       = "3603",
 doi          = "10.1007/11541868\_19",
)
@inproceedings(schimpf:construction,
 author       = "Alexander Schimpf and Stephan Merz and Jan-Georg Smaus",
 year         = "2009",
 title        = "Construction of {B\"uchi} Automata for {LTL} Model Checking Verified in {I}sabelle/{HOL}",
 editor       = "Tobias Nipkow and Christian Urban",
 booktitle    = "22nd Intl. Conf. Theorem Proving in Higher-Order Logics (TPHOLs 2009)",
 series       = "Lecture Notes in Computer Science",
 volume       = "5674",
 publisher    = "Springer",
 address      = "Munich, Germany",
 doi          = "10.1007/978-3-642-03359-9\_29",
 url          = "http://www.loria.fr/~merz/papers/tphols2009.html",
)
@article(Schmidt-SchaubB:1991:ACD:114341.114342,
 author       = "Manfred Schmidt-Schaub\ss  and Gert Smolka",
 year         = "1991",
 title        = "Attributive concept descriptions with complements",
 journal      = "Artif. Intell.",
 volume       = "48",
 number       = "1",
 pages        = "1--26",
 doi          = "10.1016/0004-3702(91)90078-X",
)
@inproceedings(Tsarkov2006,
 author       = "Dmitry Tsarkov and Ian Horrocks",
 year         = "2006",
 title        = "FaCT++ Description Logic Reasoner: System Description",
 booktitle    = "Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2006)",
 series       = "Lecture Notes in Artificial Intelligence",
 volume       = "4130",
 publisher    = "Springer",
 pages        = "292--297",
 doi          = "10.1007/11814771\_26",
)
@mastersthesis(wind01:_modal_logic,
 author       = "Paulien de Wind",
 year         = "2001",
 title        = "Modal Logic",
 school       = "Vrije Universiteit Amsterdam",
)