Forschungsprojekte

Description Logics (DLs) are a well-investigated family of logic-based knowledge representation languages, which are, e.g., frequently used to formalize ontologies for application domains such as biology and medicine. To define the important notions of such an application domain as formal concepts, DLs state necessary and sufficient conditions for an individual to belong to a concept. Once the relevant concepts of an application domain are formalized this way, they can be used in queries in order to retrieve new information from data. Since traditional DLs are based on classical first-order logic, their semantics is strict in the sense that all the stated properties need to be satisfied for an individual to belong to a concept, and the same is true for answers to queries. In applications where exact definitions are hard to come by, it would be useful to relax this strict requirement and allow for approximate definitions of concepts, where most, but not all, of the stated properties are required to hold. Similarly, if a query has no exact answer, approximate answers that satisfy most of the features the query is looking for could be useful.In order to allow for approximate definitions of concepts, we have introduced the notion of a graded membership function, which instead of a Boolean membership value 0 or 1 yields a membership degree from the interval [0,1]. Threshold concepts can then, for example, require that an individual belongs to a concept C with degree at least 0.8. A different approach, which is based on the use of similarity measures on concepts, was used to relax instance queries (i.e., queries that consist of a single concept). Given a query concept C, we are looking for answers to queries D whose similarity to C is higher than a certain threshold. While these two approaches were developed independently by the two applicants together with doctoral students, it has turned out that there are close connections. Similarity measures can be used to define graded membership functions, and threshold concepts w.r.t. these functions provide a more natural semantics for relaxed instance queries.The goals of this project are to1. explore the connection between the two approaches in detail, and develop and investigate a combined approach; 2. extend the applicability of this combined approach by considering a) more expressive DLs than the DL EL for which the approaches were initially developed; b) more general terminological formalisms; c) more general queries such as conjunctive queries; d) more general inference problems such as determining appropriate threshold values rather than requiring the user to provide them; 3. conduct an empirical study to a) evaluate the approach on a prototypical application; b) generate appropriate graded membership functions or similarity measures using automated parameter tuning approaches.

Further Information

More and more information on individuals (e.g., persons, events, biological objects) are available electronically in a structured or semi-structured form. Selecting individuals satisfying certain constraints based on such data manually is a complex, error-prone, and time and personnel-consuming effort. For this reason, tools that can automatically or semi-automatically answer questions based on the available data need to be developed. While simple questions can directly be expressed and answered using keywords in natural language, complex questions that can refer to type and relational information increase the precision of the retrieved results, and thus reduce the effort for posterior manual verification of the results. One example for this situation is the setting where electronic patient records are used to find patients satisfying non-trivial combinations of certain properties, such as eligibility criteria for clinical trials. Another example that will also be considered as a use case in this project is the setting where a student asks the examination office questions about study and examination regulations. In both cases, the original question is formulated in natural language.In the GoAsq project, we will investigate, compare, and finally combine two different approaches for answering questions formulated in natural language over textual, semi-structured, and structured data. One approach uses the expertise in text-based question answering of the French partners to directly answer natural language questions using natural language processing and information retrieval techniques. The other tries to translate the natural language questions into formal, database-like queries and then answer these formal queries w.r.t. a domain-dependent ontology using database techniques. The automatic translation is required since it would be quite hard for the people asking the questions (medical doctors, students) to formulate them as formal queries. The ontology allows to overcome the possible semantic mismatch between the person producing the source data (e.g., the GPs writing the clinical notes) and the person formulating the question (e.g., the researcher formulating the trial criteria). GoAsq can thus leverage recent advances obtained in the ontology community on accessing data through ontologies, called ontology-based query answering (OBQA). More precisely, in Task 1 of the project we investigate the two use cases mentioned above (eligibility criteria; study regulations). In Task 2 we will introduce and analyze extensions to existing formal query languages that are required by these use cases. Task 3 will develop techniques for extracting formal queries from textual queries, and Task 4 will evaluate the approach obtained this way, compare it with approaches for text-based question answering, and develop a hybrid approach that combines the advantages of both.

Further Information

DFG Project: Reasoning in Fuzzy Description Logics with General Concept Inclusion Axioms 
Principal Investigators: F. Baader, R. Peñaloza 
Involved person: S. Borgwardt 
Start date: May 1, 2012 
Duration years: 3 years (+ 4 month parental leave) 
Funded by: DFG

Description logics (DLs) are a family of logic-based knowledge representation languages that are tailored towards representing terminological knowledge, by allowing the knowledge engineer to define the relevant concepts of an application domain within this logic and then reason about these definitions using terminating inference algorithms. In order to deal with applications where the boundaries between members and non-members of concepts (e.g., “tall man,” “high blood pressure,” or “heavy network load”) are blurred, DLs have been combined with fuzzy logics, resulting in fuzzy description logics (fuzzy DLs). Considering the literature on fuzzy description logics of the last 20 years, one could get the impression that, from an algorithmic point of view, fuzzy DLs behave very similarly to their crisp counterparts: for fuzzy DLs based on simple t-norms such as Gödel, black-box procedures that call reasoners for the corresponding crisp DLs can be used, whereas fuzzy DLs based on more complicated t-norms (such as product and Lukasiewicz) can be dealt with by appropriately modifying the tableau-based reasoners for the crisp DLs. However, it has recently turned out that, in the presence of so-called general concept inclusion axioms (GCIs), the published extensions of tableaubased reasoners to fuzzy DLs do not work correctly. In fact, we were able to show that GCIs can cause undecidability for certain fuzzy DLs based on product t-norm. However, for most fuzzy DLs, the decidability status of reasoning w.r.t. GCIs is still open. The purpose of this project is to investigate the border between decidability and undecidability for fuzzy DLs with GCIs. On the one hand, we will try to show more undecidability results for specific fuzzy DLs, and then attempt to derive from these results general criteria that imply undecidability. On the other hand, we will try to determine decidable special cases, by extending tableau- and automatabased decision procedures for DLs to the fuzzy case, and also looking at other reasoning approaches for inexpressive DLs. 

Publications on the topics of this project can be found on our publications web page.

Further Information

PhD Project: Temporalised Description Logics with Good Algorithmic Properties, and Their Application for Monitoring Partially Observable Events 
Principal Investigator: F. Baader 
Involved person: M. Lippmann 
Start date: July 1, 2010 
Funded by: TU Dresden

Using the temporalised Description Logic ALC-LTL as a starting point, this work has as objective to investigate different kinds of extensions of this logic. The main focus will be on decidability results, the complexity of the satisfiability problem, and their usefulness for runtime monitoring. To this end, it is essential to understand the formal properties of such temporal Description Logics.

Publications on the topics of this project can be found on our publications web page.

DFG Project: Unification in Description Logics for Avoiding Redundancies in Medical Ontologies 
Principal Investigator: F. Baader 
Involved person: B. Morawska, S. Borgwardt, J. Mendez 
Start date: July 1, 2009 
Duration: 3 years 
Funded by: DFG

Unification in Description Logics can be used to discover redundancies in ontologies. Up to now the unification procedure has been available only for the description logic FL0 that does not have any applications in medical ontologies. The unification in FL0 has bad complexity, and all attempts to extend this procedure to other description logics has failed up to now. We have developed recently the algorithm for unification in the description logic EL. The procedure has better complexity than that for FL0. Medical ontologies (e.g. SNOMED CT) use EL as the language of knowledge representation and the problem of redundancy occurs in them in practice.

In this project we will optimize and implement the new algorithm for the unification in EL. We will show, with the examples from SNOMED CT, how the redundancies can be discovered and removed. We will also attempt to extend the algorithm to some extensions of EL that are important for practical applications. We will define and analyze equational theories for which the procedure for EL-unification can be extended, in order to discover possible syntactic criteria that enable such extensions.

Publications on the topics of this project can be found on our publications web page.

Further Information

DFG Project: Completing knowledge bases using Formal Concept Analysis 
Principal Investigator: F. Baader 
Involved persons: J. Mendez, B. Sertkaya 
Start date: November 15, 2007 
Duration: 2 years 
Funded by: DFG

Description Logics are employed in various application domains, such as natural language processing, configuration, databases, and bio-medical ontologies, but their most notable success so far is due to the fact that DLs provide the logical underpinning of OWL, the standard ontology language for the semantic web. As a consequence of this standardization, ontologies written in OWL are employed in more and more applications. As the size of these ontologies grows, tools that support improving their quality becomes more important. The tools available until now use DL reasoning to detect inconsistencies and to infer consequences, i.e., implicit knowledge that can be deduced from the explicitly represented knowledge. These approaches address the quality dimension of soundness of an ontology, both within itself (consistency) and w.r.t. the intended application domain. In this project we are concerned with a different quality dimension: completeness. We aim to develop formally well-founded techniques and tools that support the ontology engineer in checking whether an ontology contains all the relevant information about the application domain, and to extend the ontology appropriately if this is not the case.

Literature:

Daniel Borchmann and Felix Distel: Mining of EL-GCIs. In The 11th IEEE International Conference on Data Mining Workshops. Vancouver, Canada, IEEE Computer Society, 11 December 2011.

Felix Distel: Learning Description Logic Knowledge Bases from Data using Methods from Formal Concept Analysis. PhD Thesis, TU Dresden, Germany, April 2011.

Felix Distel and Barış Sertkaya: On the complexity of enumerating pseudo-intents. Discrete Applied Mathematics, 159(6):450–466, 2011.

Felix Distel: An Approach to Exploring Description Logic Knowledge Bases. In Barış Sertkaya and Léonard Kwuida, editors, Proceedings of the 8th International Conference on Formal Concept Analysis, (ICFCA 2010), volume 5986 of in Lecture Notes in Artificial Intelligence, pages 209–224. Springer, 2010.

Felix Distel: Hardness of Enumerating Pseudo-Intents in the Lectic Order. In Barış Sertkaya and Léonard Kwuida, editors, Proceedings of the 8th International Conference on Formal Concept Analysis, (ICFCA 2010), volume 5986 of in Lecture Notes in Artificial Intelligence, pages 124–137. Springer, 2010.

Bernardo Cuenca Grau, Christian Halaschek-Wiener, Yevgeny Kazakov, and Boontawee Suntisrivaraporn: Incremental classification of description logics ontologies. J. of Automated Reasoning, 44(4):337–369, 2010.

Rafael Peñaloza and Barış Sertkaya: On the Complexity of Axiom Pinpointing in the EL Family of Description Logics. In Fangzhen Lin, Ulrike Sattler, and Miroslaw Truszczynski, editors, Proceedings of the Twelfth International Conference on Principles of Knowledge Representation and Reasoning (KR 2010). AAAI Press, 2010.

Franz Baader and Felix Distel: Exploring Finite Models in the Description Logic ELgfp. In Sébastien Ferré and Sebastian Rudolph, editors, Proceedings of the 7th International Conference on Formal Concept Analysis, (ICFCA 2009), volume 5548 of in Lecture Notes in Artificial Intelligence, pages 146–161. Springer Verlag, 2009.

Franz Baader and Barış Sertkaya: Usability Issues in Description Logic Knowledge Base Completion. In Sébastien Ferré and Sebastian Rudolph, editors, Proceedings of the 7th International Conference on Formal Concept Analysis, (ICFCA 2009), volume 5548 of in Lecture Notes in Artificial Ingelligence, pages 1–21. Springer Verlag, 2009.

Barış Sertkaya: OntoComP System Description. In Bernardo Cuenca Grau, Ian Horrocks, Boris Motik, and Ulrike Sattler, editors, Proceedings of the 2009 International Workshop on Description Logics (DL2009), volume 477 of in CEUR-WS, 2009.

Barış Sertkaya: OntoComP: A Protege Plugin for Completing OWL Ontologies. In Proceedings of the 6th European Semantic Web Conference, (ESWC 2009), volume 5554 of in Lecture Notes in Computer Science, pages 898–902. Springer Verlag, 2009.

Barış Sertkaya: Some Computational Problems Related to Pseudo-intents. In Sébastien Ferré and Sebastian Rudolph, editors, Proceedings of the 7th International Conference on Formal Concept Analysis, (ICFCA 2009), volume 5548 of in Lecture Notes in Artificial Intelligence, pages 130–145. Springer Verlag, 2009.

Barış Sertkaya: Towards the Complexity of Recognizing Pseudo-intents. In Frithjof Dau and Sebastian Rudolph, editors, Proceedings of the 17th International Conference on Conceptual Structures, (ICCS 2009), pages 284–292, 2009.

Franz Baader and Felix Distel: A Finite Basis for the Set of EL-Implications Holding in a Finite Model. In Raoul Medina and Sergei Obiedkov, editors, Proceedings of the 6th International Conference on Formal Concept Analysis, (ICFCA 2008), volume 4933 of in Lecture Notes in Artificial Intelligence, pages 46–61. Springer, 2008.

Franz Baader and Boontawee Suntisrivaraporn: Debugging SNOMED CT Using Axiom Pinpointing in the Description Logic EL⁺. In Proceedings of the 3rd Knowledge Representation in Medicine (KR-MED'08): Representing and Sharing Knowledge Using SNOMED, volume 410 of in CEUR-WS, 2008.

Miki Hermann and Barış Sertkaya: On the Complexity of Computing Generators of Closed Sets. In Raoul Medina and Sergei A. Obiedkov, editors, Proceedings of the 6th International Conference on Formal Concept Analysis, (ICFCA 2008), volume 4933 of in Lecture Notes in Computer Science, pages 158–168. Springer Verlag, 2008.

Boontawee Suntisrivaraporn: Module Extraction and Incremental Classification: A Pragmatic Approach for EL⁺ Ontologies. In Sean Bechhofer, Manfred Hauswirth, Joerg Hoffmann, and Manolis Koubarakis, editors, Proceedings of the 5th European Semantic Web Conference (ESWC'08), volume 5021 of in Lecture Notes in Computer Science, pages 230–244. Springer-Verlag, 2008.

Franz Baader, Bernhard Ganter, Ulrike Sattler, and Baris Sertkaya: Completing Description Logic Knowledge Bases using Formal Concept Analysis. In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI-07). AAAI Press, 2007.

Franz Baader, Rafael Peñaloza, and Boontawee Suntisrivaraporn: Pinpointing in the Description Logic EL. In Proceedings of the 30th German Conference on Artificial Intelligence (KI2007), volume 4667 of in Lecture Notes in Artificial Intelligence, pages 52–67. Osnabrück, Germany, Springer-Verlag, 2007.

Further Information

PhD Project: Knowledge Acquisition in Description Logics by Means of Formal Concept Analysis 
Principal Investigator: F. Baader 
Involved persons: F. Distel, D. Borchmann 
Start date: May 1, 2007 
Funded by: Cusanuswerk e.V. (until April 30, 2009) and TU Dresden

This work's objective is making the capabilities of Formal Concept Analysis applicable in Description Logics. The major interest will be on supporting ontology engineers in defining new concepts. At first glance Formal Concept Analysis appears to be a good starting point for this. However, a deeper examination shows that there are grave differences between concepts in FCA and concepts in DL. These differences make it necessary to extend and modify the Theory of Formal Concept Analysis. The major discrepancies lie in expressiveness with respect to intensional concept descriptions and in the contrast between open-world semantics and closed-world semantics. We try to expand Formal Concept Analysis in this direction.

Literature:

Felix Distel: Learning Description Logic Knowledge Bases from Data using Methods from Formal Concept Analysis. PhD Thesis, TU Dresden, Germany, April 2011.

Felix Distel: An Approach to Exploring Description Logic Knowledge Bases. In Barış Sertkaya and Léonard Kwuida, editors, Proceedings of the 8th International Conference on Formal Concept Analysis, (ICFCA 2010), volume 5986 of in Lecture Notes in Artificial Intelligence, pages 209–224. Springer, 2010.

Franz Baader and Felix Distel: Exploring Finite Models in the Description Logic ELgfp. In Sébastien Ferré and Sebastian Rudolph, editors, Proceedings of the 7th International Conference on Formal Concept Analysis, (ICFCA 2009), volume 5548 of in Lecture Notes in Artificial Intelligence, pages 146–161. Springer Verlag, 2009.

Franz Baader and Felix Distel: A Finite Basis for the Set of EL-Implications Holding in a Finite Model. In Raoul Medina and Sergei Obiedkov, editors, Proceedings of the 6th International Conference on Formal Concept Analysis, (ICFCA 2008), volume 4933 of in Lecture Notes in Artificial Intelligence, pages 46–61. Springer, 2008.

DFG Project: Description Logics with Existential Quantifiers and Polynomial Subsumption Problem and Their Applications in Bio-Medical Ontologies 
Principal Investigator: F. Baader 
Involved persons: M. Lippmann, C. Lutz, B. Suntisrivaraporn. 
Start date: June 1, 2006 
Duration: 2 years + 1 year extension 
Funded by: Deutsche Forschungsgemeinschaft (DFG), Project BA 1122/11-1

Description logics (DLs) with value restrictions have so far been well-investigated. In particular, every expressive DLs, together with practical algorithms, have been developed. Despite having high worst-case complexity, their highly optimized implementations behave well in practice. However, it has turned out that, in bio-medical ontology applications, inexpressive DLs with existential restrictions, but without value restrictions, suffice. In the scope of this project, DLs with existential restrictions shall be investigated, both theoretically and practically. This includes identifying the polynomial borders of subsumption problems, developing optimizations for the subsumption algorithms, evaluating against realistic large-scale bio-medical ontologies. Moreover, supplemental reasoning problems (e.g., conjunctive queries) shall be investigated.

Literature:

Julian Mendez: A classification algorithm for ELHIf_R⁺. Master Thesis, TU Dresden, Germany, 2011.

Julian Mendez, Andreas Ecke, and Anni-Yasmin Turhan: Implementing completion-based inferences for the el-family. In Riccardo Rosati, Sebastian Rudolph, and Michael Zakharyaschev, editors, Proceedings of the international Description Logics workshop. CEUR, 2011.

Franz Baader, Meghyn Bienvenu, Carsten Lutz, and Frank Wolter: Query and Predicate Emptiness in Description Logics. In Fangzhen Lin and Ulrike Sattler, editors, Proceedings of the 12th International Conference on Principles of Knowledge Representation and Reasoning (KR2010). AAAI Press, 2010.

Franz Baader, Carsten Lutz, and Anni-Yasmin Turhan: Small is again Beautiful in Description Logics. KI – Künstliche Intelligenz, 24(1):25–33, 2010.

Boris Konev, Carsten Lutz, Denis Ponomaryov, and Frank Wolter: Decomposing description logic ontologies. In Fangzhen Lin, Ulrike Sattler, and Miroslaw Trusz- czynski, editors, Proceedings of the Twelfth International Conference on Principles of Knowledge Representation and Reasoning (KR2010). AAAI Press, 2010.

Carsten Lutz and Frank Wolter. Deciding inseparability and conservative extensions in the description logic EL. Journal of Symbolic Computation, 45(2):194–228, 2010.

Roman Kontchakov, Carsten Lutz, David Toman, Frank Wolter, and Michael Zakharyaschev: The combined approach to query answering in DL-Lite. In Fangzhen Lin, Ulrike Sattler, and Miroslaw Truszczynski, editors, Proceedings of the Twelfth International Conference on Principles of Knowledge Representation and Reasoning (KR2010). AAAI Press, 2010.

Franz Baader, Stefan Schulz, Kent Spackmann, and Bontawee Suntisrivaraporn: How Should Parthood Relations be Expressed in SNOMED CT?. In Proceedings of 1. Workshop des GI-Arbeitskreises Ontologien in Biomedizin und Lebenswissenschaften (OBML 2009), 2009.

Carsten Lutz, David Toman, and Frank Wolter: Conjunctive query answering in the description logic EL using a relational database system. In Craig Boutilier, editor, Proc. of the 21st Int. Joint Conf. on Artificial Intelligence (IJCAI 2009), pages 2070–2075. IJCAI/AAAI, 2009.

Julian Mendez and Boontawee Suntisrivaraporn: Reintroducing CEL as an OWL 2 EL Reasoner. In Bernardo Cuenca Grau, Ian Horrocks, Boris Motik, and Ulrike Sattler, editors, Proceedings of the 2009 International Workshop on Description Logics (DL2009), volume 477 of in CEUR-WS, 2009.

Boris Motik, Bernardo Cuenca Grau, Ian Horrocks, Zhe Wu, and Carsten Lutz, editors: OWL 2 Web Ontology Language: Profiles. W3C Recommendation, 27 October 2009. Available at http://www.w3.org/TR/owl-profiles/.

Stefan Schulz, Boontawee Suntisrivaraporn, Franz Baader, and Martin Boeker: SNOMED reaching its adolescence: Ontologists' and logicians' health check. International Journal of Medical Informatics, 78(Supplement 1):S86–S94, 2009.

Franz Baader, Sebastian Brandt, and Carsten Lutz: Pushing the EL Envelope Further. In Kendall Clark and Peter F. Patel-Schneider, editors, In Proceedings of the OWLED 2008 DC Workshop on OWL: Experiences and Directions, 2008.

Christoph Haase and Carsten Lutz: Complexity of Subsumption in the EL Family of Description Logics: Acyclic and Cyclic TBoxes. In Malik Ghallab, Constantine D. Spyropoulos, Nikos Fakotakis, and Nikos Avouris, editors, Proceedings of the 18th European Conference on Artificial Intelligence (ECAI08), volume 178 of in Frontiers in Artificial Intelligence and Applications, pages 25–29. IOS Press, 2008.

Boris Konev, Carsten Lutz, Dirk Walther, and Frank Wolter: Semantic Modularity and Module Extraction in Description Logics. In Malik Ghallab, Constantine D. Spyropoulos, Nikos Fakotakis, and Nikos Avouris, editors, Proceedings of the 18th European Conference on Artificial Intelligence (ECAI08), volume 178 of in Frontiers in Artificial Intelligence and Applications, pages 55–59. IOS Press, 2008.

Boontawee Suntisrivaraporn: Module Extraction and Incremental Classification: A Pragmatic Approach for EL⁺ Ontologies. In Sean Bechhofer, Manfred Hauswirth, Joerg Hoffmann, and Manolis Koubarakis, editors, Proceedings of the 5th European Semantic Web Conference (ESWC'08), volume 5021 of in Lecture Notes in Computer Science, pages 230–244. Springer-Verlag, 2008.

Quoc Huy Vu: Subsumption in the description logic ELHIf_R⁺. Master Thesis, TU Dresden, Germany, 2008.

A. Artale, R. Kontchakov, C. Lutz, F. Wolter, and M. Zakharyaschev: Temporalising Tractable Description Logics. In Proceedings of the Fourteenth International Symposium on Temporal Representation and Reasoning. IEEE Computer Society Press, 2007.

Adila Krisnadhi and Carsten Lutz: Data Complexity in the EL family of Description Logics. In Nachum Dershowitz and Andrei Voronkov, editors, Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR2007), volume 4790 of in Lecture Notes in Artificial Intelligence, pages 333–347. Springer-Verlag, 2007.

Christoph Haase: Complexity of subsumption in extensions of EL. Master Thesis, TU Dresden, Germany, 2007.

Carsten Lutz, Dirk Walther, and Frank Wolter: Conservative Extensions in Expressive Description Logics. In Manuela Veloso, editor, Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI'07), pages 453–458. AAAI Press, 2007.

Carsten Lutz and Frank Wolter: Conservative Extensions in the Lightweight Description Logic EL. In Frank Pfenning, editor, Proceedings of the 21th Conference on Automated Deduction (CADE-21), volume 4603 of in Lecture Notes in Artificial Intelligence, pages 84–99. Springer-Verlag, 2007.

Stefan Schulz, Boontawee Suntisrivaraporn, and Franz Baader: SNOMED CT's Problem List: Ontologists' and Logicians' Therapy Suggestions. In , editor, Proceedings of The Medinfo 2007 Congress, volume of in Studies in Health Technology and Informatics (SHTI-series), page . IOS Press, 2007.

Boontawee Suntisrivaraporn, Franz Baader, Stefan Schulz, and Kent Spackman: Replacing SEP-Triplets in SNOMED CT using Tractable Description Logic Operators. In Jim Hunter Riccardo Bellazzi, Ameen Abu-Hanna, editor, Proceedings of the 11th Conference on Artificial Intelligence in Medicine (AIME'07), volume of in Lecture Notes in Computer Science, page . Springer-Verlag, 2007.

F. Baader, C. Lutz, and B. Suntisrivaraporn: Efficient Reasoning in EL⁺. In Proceedings of the 2006 International Workshop on Description Logics (DL2006), in CEUR-WS, 2006.

F. Baader, C. Lutz, and B. Suntisrivaraporn: CEL—A Polynomial-time Reasoner for Life Science Ontologies. In U. Furbach and N. Shankar, editors, Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06), volume 4130 of in Lecture Notes in Artificial Intelligence, pages 287–291. Springer-Verlag, 2006.

F. Baader, C. Lutz, and B. Suntisrivaraporn: Is Tractable Reasoning in Extensions of the Description Logic EL Useful in Practice?. In Proceedings of the Methods for Modalities Workshop (M4M-05), 2005.

Further Information

DFG Project: Explaining Ontology Consequences 
Principal Investigator: F. Baader 
Involved person: R. Peñaloza 
Start date: April 1, 2006 
Duration: 2.5 years 
Funded by: Deutsche Forschungsgemeinschaft (DFG) Graduiertenkolleg GRK 446

The objective of this work is to develop methods for finding small (preferably minimal) sub-ontologies from which a given consequence follows. These sub-ontologies are called explanations. The approach followed is to modify the procedures used to detect the consequence to allow for tracking the ontology axioms responsible for it. The major interest is on supporting Knowledge Engineers in diagnosing and correcting errors in the built ontologies.

Literature

Franz Baader and Rafael Peñaloza: Automata-Based Axiom Pinpointing. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Proceedings of the 4th International Joint Conference on Automated Reasoning, (IJCAR 2008), volume 5195 of in Lecture Notes in Artificial Intelligence, pages 226–241. Springer, 2008.

Franz Baader and Boontawee Suntisrivaraporn: Debugging SNOMED CT Using Axiom Pinpointing in the Description Logic EL⁺. In Proceedings of the 3rd Knowledge Representation in Medicine (KR-MED'08): Representing and Sharing Knowledge Using SNOMED, volume 410 of in CEUR-WS, 2008.

Rafael Peñaloza: Automata-based Pinpointing for DLs. In Proceedings of the 2008 International Workshop on Description Logics (DL2008), volume 353 of in CEUR-WS, 2008.

Franz Baader and Rafael Peñaloza: Axiom Pinpointing in General Tableaux. In N. Olivetti, editor, Proceedings of the 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods TABLEAUX 2007, volume 4548 of in Lecture Notes in Computer Science, pages 11–27. Aix-en-Provence, France, Springer-Verlag, 2007.

Franz Baader, Rafael Peñaloza, and Boontawee Suntisrivaraporn: Pinpointing in the Description Logic EL. In Proceedings of the 2007 International Workshop on Description Logics (DL2007), in CEUR-WS, 2007.

DFG Project: Action Formalisms with Description Logic 
Principal Investigators: F. Baader, M. Thielscher 
Involved persons: C. Drescher, H. Liu, C. Lutz, M. Lippmann, M. Milicic 
Start date: September 1, 2005 
Duration: 2 years + 2 years extension 
Project Partners: University of Leipzig (Germany), Aachen University of Technology (Germany), University of Freiburg(Germany) 
Funded by: Deutsche Forschungsgemeinschaft (DFG), Project BA 1122/13

The aim of this project is the integration of description logic and action formalisms. The motivation for this integration is twofold. On the one hand, general action calculi like the fluent calculus and the situation calculus are based on full first order logic. This entails undecidability in general of basic reasoning tasks like e.g. checking state consistency, action applicability or computing updated states. By identifying suitable description logics for describing the current world state these issues may be adressed. On the other hand, the need for integrating some kind of action representation into description logics has arisen. Description logics are a highly successful static knowledge representation formalism with applications e.g. on the semantic web or in the life sciences. Clearly, it is desirable to have the means to model semantic web services or reason about dynamic domains in the life sciences, like e.g. clinical protocols. 

Another objective of this project is to develop a version of the logic programming paradigm designed specifically for programming intelligent agents. This may be thought of as adapting the successful constraint-logic programming scheme CLP(X) to CLP(Sigma), where Sigma is a domain axiomatization in an action calculus. Of course, for this it is of tantamount importance that the special atoms of the logic program can effectively be decided via the underlying domain axiomatization. The resulting scheme instantiated with the action calculi developed in the afore-mentioned steps can then be implemented by combining the mature technologies of both plain prolog and description logic reasoners. The system will be evaluated by modeling semantic web services or clinical protocols.

Literature:

Hongkai Liu, Carsten Lutz, Maja Milicic, and Frank Wolter: Foundations of instance level updates in expressive description logics. Artificial Intelligence, 175(18):2170–2197, 2011.

M. Thielscher: A unifying action calculus. Artificial Intelligence, 175(1):120–141, 2011.

Franz Baader, Marcel Lippmann, and Hongkai Liu: Using Causal Relationships to Deal with the Ramification Problem in Action Formalisms Based on Description Logics. In Christian G. Fermüller and Andrei Voronkov, editors, Proceedings of the 17th International Conference on Logic for Programming, Artifical Intelligence, and Reasoning (LPAR-17), volume 6397 of in Lecture Notes in Computer Science (subline Advanced Research in Computing and Software Science), pages 82–96. Yogyakarta, Indonesia, Springer-Verlag, October 2010.

Franz Baader, Hongkai Liu, and Anees ul Mehdi: Verifying Properties of Infinite Sequences of Description Logic Actions. In Helder Coelho, Rudi Studer, and Michael Wooldridge, editors, Proceedings of the 19th European Conference on Artificial Intelligence (ECAI10), volume 215 of in Frontiers in Artificial Intelligence and Applications, pages 53–58. IOS Press, 2010.

C. Drescher: Action Logic Programs — How to Specify Strategic Behavior in Dynamic Domains Using Logical Rules. PhD thesis, TU Dresden, Germany, 2010.

Hongkai Liu: Updating Description Logic ABoxes. PhD thesis, TU Dresden, Germany, 2010.

Franz Baader, Andreas Bauer, and Marcel Lippmann: Runtime Verification Using a Temporal Description Logic. In Silvio Ghilardi and Roberto Sebastiani, editors, Proceedings of the 7th International Symposium on Frontiers of Combining Systems (FroCoS 2009), volume 5749 of in Lecture Notes in Computer Science, pages 149–164. Springer-Verlag, 2009.

Conrad Drescher, Hongkai Liu, Franz Baader, Steffen Guhlemann, Uwe Petersohn, Peter Steinke, and Michael Thielscher: Putting ABox Updates into Action. In Silvio Ghilardi and Roberto Sebastiani, editors, The Seventh International Symposium on Frontiers of Combining Systems (FroCoS-2009), volume 5749 of in Lecture Notes in Computer Science, pages 149–164. Springer-Verlag, 2009.

Conrad Drescher, Hongkai Liu, Franz Baader, Peter Steinke, and Michael Thielscher: Putting ABox Updates into Action. In Proceedings of the 8th IJCAI International Workshop on Nonmontonic Reasoning, Action and Change (NRAC-09), 2009.

C. Drescher, S. Schiffel, and M. Thielscher: A declarative agent programming language based on action theories. In Ghilardi, S. and Sebastiani, R., editors, Proceedings of the Seventh International Symposium on Frontiers of Combining Systems (FroCoS 2009), volume 5749 of LNCS, pages 230–245, Trento, Italy. Springer, 2009.

A. ul Mehdi: Integrate action formalisms into linear temporal logics. Master thesis, TU Dresden, Germany, 2009.

Franz Baader, Silvio Ghilardi, and Carsten Lutz: LTL over Description Logic Axioms. In Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR2008), 2008.

C. Drescher and M. Thielscher: A fluent calculus semantics for ADL with plan constraints. In Hölldobler, S., Lutz, C., and Wansing, H., editors, Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA08), volume 5293 of LNCS, pages 140–152, Dresden, Germany. Springer, 2008.

Hongkai Liu, Carsten Lutz, and Maja Milicic: The Projection Problem for EL Actions. In Proceedings of the 2008 International Workshop on Description Logics (DL2008), volume 353 of in CEUR-WS, 2008.

Y. Bong: Description Logic ABox Updates Revisited. Master thesis, TU Dresden, Germany, 2007.

C. Drescher and M. Thielscher: Integrating action calculi and description logics. In Hertzberg, J., Beetz, M., and Englert, R., editors, Proceedings of the 30th Annual German Conference on Artificial Intelligence (KI 2007), volume 4667 of LNCS, pages 68–83, Osnabrück, Germany. Springer, 2007.

Conrad Drescher and Michael Thielscher: Reasoning about actions with description logics. In P. Peppas and M.-A. Williams, editors, Proceedings of the 7th IJCAI International Workshop on Nonmonotonic Reasoning, Action and Change (NRAC 2007), Hyderabad, India, January 2007.

H. Liu, C. Lutz, M. Milicic, and F. Wolter: Description Logic Actions with general TBoxes: a Pragmatic Approach. In Proceedings of the 2006 International Workshop on Description Logics (DL2006), 2006.

H. Liu, C. Lutz, M. Milicic, and F. Wolter: Reasoning about Actions using Description Logics with general TBoxes. In Michael Fisher, Wiebe van der Hoek, Boris Konev, and Alexei Lisitsa, editors, Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA 2006), volume 4160 of in Lecture Notes in Artificial Intelligence, pages 266–279. Springer-Verlag, 2006.

H. Liu, C. Lutz, M. Milicic, and F. Wolter: Updating Description Logic ABoxes. In Patrick Doherty, John Mylopoulos, and Christopher Welty, editors, Proceedings of the Tenth International Conference on Principles of Knowledge Representation and Reasoning (KR'06), pages 46–56. AAAI Press, 2006.

Michael Thielscher and Thomas Witkowski: The Features-and-Fluents semantics for the fluent calculus. In P. Doherty, J. Mylopoulos, and C. Welty, editors, Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 362–370, Lake District, UK, June 2006.

F. Baader, C. Lutz, M. Milicic, U. Sattler, and F. Wolter: A Description Logic Based Approach to Reasoning about Web Services. In Proceedings of the WWW 2005 Workshop on Web Service Semantics (WSS2005), 2005.

F. Baader, C. Lutz, M. Milicic, U. Sattler, and F. Wolter: Integrating Description Logics and Action Formalisms: First Results. In Proceedings of the 2005 International Workshop on Description Logics (DL2005), number 147 in CEUR-WS, 2005.

F. Baader, C. Lutz, M. Milicic, U. Sattler, and F. Wolter: Integrating Description Logics and Action Formalisms: First Results. In Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-05), 2005.

Further Information

Further Information

EU Project: TONES (Thinking Ontologies) 
Principal Investigator: F. Baader 
Involved persons: C. Lutz, M. Milicic, B. Sertkaya, B. Suntisrivaraporn, A.-Y. Turhan. 
Start date: September 1, 2005 
Duration: 3 years 
Project Partners: Free University of Bolzano (Italy), Università degli Studi di Roma "La Sapienza" (Italy), The University of Manchester (UK), Technische Universität Hamburg-Harburg (Germany) 
Funded by: EU (FP6-7603)

Ontologies are seen as the key technology used to describe the semantics of information at various sites, overcoming the problem of implicit and hidden knowledge and thus enabling exchange of semantic contents. As such, they have found applications in key growth areas, such as e-commerce, bio-informatics, Grid computing, and the Semantic Web.

The aim of the project is to study and develop automated reasoning techniques for both offline and online tasks associated with ontologies, either seen in isolation or as a community of interoperating systems, and devise methodologies for the deployment of such techniques, on the one hand in advanced tools supporting ontology design and management, and on the other hand in applications supporting software agents in operating with ontologies. 

Literature can be found here.

Reports on the TONES project appeared in the following news:

• the ACM tech news (Dec. 2009)
• L'ATELIER—a french on-line magazine (Nov. 2009)

Konkretes Ziel der zweiten Projektphase soll daher sein, verschiedene Ansätze zur Entwicklung von Entscheidungsalgorithmen für Logiken zu vergleichen und miteinander zu integrieren. Insbesondere sollen hier tableau- und automatenbasierte Verfahren für Beschreibungs- und Modallogiken sowie GF untersucht werden, mit dem Ziel einen einheitlichen algorithmischen Ansatz zu erhalten, der die Vorteile beider Verfahren aufweist. Die so erhaltenen Algorithmen sollen wieder prototypisch implementiert und evaluiert werden. Ein weiteres Ziel ist die Konstruktion effizienter Algorithmen für das Auswertungsproblem dieser Logiken. Schließlich soll für die hier betrachteten Logiken der Zusammenhang zwischen der Struktur von formeln und ihren algorithmischen Eigenschaften analysiert werden. Solche Resultate sollen einerseits dazu dienen, effizient entscheidbare Fragmente in diesen Logiken zu isolieren, sie sollen andererseits eine Basis zur Konstruktion Wahrscheinlichkeitsverteilungen von Formeln liefern, unter denen das average-case Verhalten von Entscheidungsverfahren analysiert werden kann.

Further Information

DFG Project: Logik-Algorithmen in der Wissensrepräsentation 
Principal Investigator: F. Baader 
Involved persons: S. Tobies, J. Hladik 
Funded by: Deutsche Forschungsgemeinschaft (DFG)

The aim of this project is the construction of decision procedures and the study of complexity issues of decision problems which are relevant for applications in the area of knowledge representation. In contrast to well-known explorations in the context of the classical Decision Problem of mathematical logic (prefix signature classes), the relevant classes of formulae are characterized by different criteria: on the one hand, the restriction to formulae with few variables or limited quantification is important, on the other hand, certain constructs (fixed points, transitive closure, number restrictions...) which are not dealt with in the classical framework are of interest.

During the first phase of this project, guarded logics, in particular the "Guarded Fragment" (GF) and its extensions, were identified as a class of logics which are relevant for for knowledge representation and very expressive but retain stable decidability properties. Moreover, practical tableau-based decision procedures for GF and expressive description logics were developed and implemented.

The practical aim of the second phase is the comparison and combination of different approaches for the development of decision procedures for logics. In particular, tableau- and automata-based procedures for GF, modal and description logics are going to be examined with the goal of a unitary algorithmical approach combining the advantages of both procedures. Another goal is the development of efficient model checking procedures for these logics.

Literature:

J. Hladik: A Tableau System for the Description Logic SHIO. In Ulrike Sattler, editor, Contributions to the Doctoral Programme of IJCAR 2004. CEUR, 2004. Available from ceur-ws.org

J. Hladik: Spinoza's Ontology. In G. Büchel, B. Klein, and T. Roth-Berghofer, editors, Proceedings of the 1st Workshop on Philosophy and Informatics (WSPI 2004), number RR-04-02 in DFKI Research Reports, 2004.

J. Hladik and J. Model: Tableau Systems for SHIO and SHIQ. In V. Haarslev and R. Möller, editors, Proceedings of the 2004 International Workshop on Description Logics (DL 2004). CEUR, 2004. Available from ceur-ws.org

F. Baader, J. Hladik, C. Lutz, and F. Wolter: From Tableaux to Automata for Description Logics. In Moshe Vardi and Andrei Voronkov, editors, Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2003), volume 2850 of in Lecture Notes in Computer Science, pages 1–32. Springer, 2003.

Franz Baader, Jan Hladik, Carsten Lutz, and Frank Wolter: From Tableaux to Automata for Description Logics. Fundamenta Informaticae, 57:1–33, 2003.

J. Hladik and U. Sattler: A Translation of Looping Alternating Automata to Description Logics. In Proc. of the 19th Conference on Automated Deduction (CADE-19), volume 2741 of in Lecture Notes in Artificial Intelligence. Springer Verlag, 2003.

Jan Hladik: Reasoning about Nominals with FaCT and RACER. In Proceedings of the 2003 International Workshop on Description Logics (DL2003), in CEUR-WS, 2003.

J. Hladik: Implementation and Optimisation of a Tableau Algorithm for the Guarded Fragment. In U. Egly and C. G. Fermüller, editors, Proceedings of the International Conference on Automated Reasoning with Tableaux and Related Methods (Tableaux 2002), volume 2381 of in Lecture Notes in Artificial Intelligence. Springer-Verlag, 2002.

G. Pan, U. Sattler, and M. Y. Vardi: BDD-Based Decision Procedures for K. In Proceedings of the Conference on Automated Deduction, volume 2392 of in Lecture Notes in Artificial Intelligence. Springer Verlag, 2002.

F. Baader and S. Tobies: The Inverse Method Implements the Automata Approach for Modal Satisfiability. In Proceedings of the International Joint Conference on Automated Reasoning IJCAR'01, volume 2083 of in Lecture Notes in Artificial Intelligence, pages 92–106. Springer-Verlag, 2001.

J. Hladik: Implementierung eines Entscheidungsverfahrens für das Bewachte Fragment der Prädikatenlogik. Diploma thesis, RWTH Aachen, Germany, 2001.

S. Tobies: Complexity Results and Practical Algorithms for Logics in Knowledge Representation. PhD thesis, RWTH Aachen, 2001.

Stephan Tobies: PSPACE Reasoning for Graded Modal Logics. Journal of Logic and Computation, 11(1):85–106, 2001.

F. Baader and U. Sattler: Tableau Algorithms for Description Logics. In R. Dyckhoff, editor, Proceedings of the International Conference on Automated Reasoning with Tableaux and Related Methods (Tableaux 2000), volume 1847 of in Lecture Notes in Artificial Intelligence, pages 1–18. St Andrews, Scotland, UK, Springer-Verlag, 2000.

C. Hirsch and S. Tobies: A Tableau Algorithm for the Clique Guarded Fragment. In Proceedings of the Workshop Advances in Modal Logic AiML 2000, 2000. Final version appeared in Advanced in Modal Logic Volume 3, 2001.

Jan Hladik: Implementing the n-ary Description Logic GF1-. In Proceedings of the International Workshop in Description Logics 2000 (DL2000), 2000.

I. Horrocks, U. Sattler, and S. Tobies: Practical Reasoning for Very Expressive Description Logics. Logic Journal of the IGPL, 8(3):239–264, 2000.

I. Horrocks, U. Sattler, and S. Tobies: Reasoning with Individuals for the Description Logic SHIQ. In David MacAllester, editor, Proceedings of the 17th International Conference on Automated Deduction (CADE-17), number 1831 in Lecture Notes in Computer Science. Germany, Springer Verlag, 2000.

I. Horrocks and S. Tobies: Reasoning with Axioms: Theory and Practice. In A. G. Cohn, F. Giunchiglia, and B. Selman, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Seventh International Conference (KR2000). San Francisco, CA, Morgan Kaufmann Publishers, 2000.

I. Horrocks, U. Sattler, S. Tessaris, and S. Tobies: How to decide Query Containment under Constraints using a Description Logic. In Andrei Voronkov, editor, Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR'2000), number 1955 in Lecture Notes in Artificial Intelligence. Springer Verlag, 2000.

U. Sattler: Description Logics for the Representation of Aggregated Objects. In W.Horn, editor, Proceedings of the 14th European Conference on Artificial Intelligence. IOS Press, Amsterdam, 2000.

Stephan Tobies: The Complexity of Reasoning with Cardinality Restrictions and Nominals in Expressive Description Logics. Journal of Artificial Intelligence Research, 12:199–217, 2000.

F. Baader, R. Molitor, and S. Tobies: Tractable and Decidable Fragments of Conceptual Graphs. In W. Cyre and W. Tepfenhart, editors, Proceedings of the Seventh International Conference on Conceptual Structures (ICCS'99), number 1640 in Lecture Notes in Computer Science, pages 480–493. Springer Verlag, 1999.

I. Horrocks and U. Sattler: A Description Logic with Transitive and Inverse Roles and Role Hierarchies. Journal of Logic and Computation, 9(3):385–410, 1999.

Ian Horrocks, Ulrike Sattler, and Stephan Tobies: Practical Reasoning for Expressive Description Logics. In Harald Ganzinger, David McAllester, and Andrei Voronkov, editors, Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR'99), number 1705 in Lecture Notes in Artificial Intelligence, pages 161–180. Springer-Verlag, September 1999.

C. Lutz, U. Sattler, and S. Tobies: A Suggestion for an n-ary Description Logic. In Patrick Lambrix, Alex Borgida, Maurizio Lenzerini, Ralf Möller, and Peter Patel-Schneider, editors, Proceedings of the International Workshop on Description Logics, number 22 in CEUR-WS, pages 81–85. Linkoeping, Sweden, Linköping University, July 30 – August 1 1999. Proceedings online available from http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-22/

S .Tobies: A NExpTime-complete Description Logic Strictly Contained in C². In J. Flum and M. Rodríguez-Artalejo, editors, Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL-99), in LNCS 1683, pages 292–306. Springer-Verlag, 1999.

S. Tobies: A PSpace Algorithm for Graded Modal Logic. In H. Ganzinger, editor, Automated Deduction – CADE-16, 16th International Conference on Automated Deduction, in LNAI 1632, pages 52–66. Trento, Italy, Springer-Verlag, July 7–10, 1999.

Further Information

Further Information

DFG Project: Novel Inference Services in Description Logics 
Principal Investigator: F. Baader 
Involved persons: S. Brandt, A.-Y. Turhan 
Funded by: Deutsche Forschungsgemeinschaft (DFG)

Over the past 15 years the area of Description Logics has seen extensive research on both theoretical and practical aspects of standard inference problems, such as subsumption and the instance problem. When DL systems were employed for practical KR-applications, however, additional inference services facilitating build-up and maintenance of large knowledge bases proved indispensible. This led to the developing of non-standard inferences such as: least common subsumer, most specific concept, approximation, and matching.

In the first project phase, non-standard inference problems have been examined w.r.t. their formal aspects, e.g. computational complexity, and have been evaluated in practice in one specific prototypical application scenario in the domain of chemical process engineering.

Building on the lessons learned during the first project phase, the second phase aims to examine how non-standard inference services can be employed in a more general application area: for the build-up, maintenance, and deployment of ontologies, e.g. for the Semantic Web. To this end, existing algorithms have to be extended considerably and new ones to be found. The more general application area moreover gives rise to additional non-standard inferences not examined during the first project phase.

The ultimate goal of this project is to gain comprehensive knowledge about the formal properties of non-standard inference problems in Description Logics and to demonstrate their utility for build-up and maintenance of knowledge bases. An additional practical goal of the second project phase is to develop a prototypical support system for a specific ontology editor, e.g. OilEd.

Literature:

Franz Baader, Barış Sertkaya, and Anni-Yasmin Turhan: Computing the Least Common Subsumer w.r.t. a Background Terminology. Journal of Applied Logic, 5(3):392–420, 2007.

F. Baader and A. Okhotin: Complexity of Language Equations With One-Sided Concatenation and All Boolean Operations. In Jordi Levy, editor, Proceedings of the 20th International Workshop on Unification, UNIF'06, pages 59–73, 2006.

F. Baader and R. Küsters: Nonstandard Inferences in Description Logics: The Story So Far. In D.M. Gabbay, S.S. Goncharov, and M. Zakharyaschev, editors, Mathematical Problems from Applied Logic I, volume 4 of in International Mathematical Series, pages 1–75. Springer-Verlag, 2006.

Carsten Lutz, Franz Baader, Enrico Franconi, Domenico Lembo, Ralf Möller, Riccardo Rosati, Ulrike Sattler, Boontawee Suntisrivaraporn, and Sergio Tessaris: Reasoning Support for Ontology Design. In Bernardo Cuenca Grau, Pascal Hitzler, Connor Shankey, and Evan Wallace, editors, In Proceedings of the second international workshop OWL: Experiences and Directions, November 2006. To appear

S. Brandt: Standard and Non-standard reasoning in Description Logics. Ph.D. Dissertation, Institute for Theoretical Computer Science, TU Dresden, Germany, 2006.

Barış Sertkaya: Computing the hierarchy of conjunctions of concept names and their negations in a Description Logic knowledge base using Formal Concept Analysis (ICFCA 2006). In Bernhard Ganter and Leonard Kwuida, editors, Contributions to ICFCA 2006, pages 73–86. Dresden, Germany, Verlag Allgemeine Wissenschaft, 2006.

Anni-Yasmin Turhan, Sean Bechhofer, Alissa Kaplunova, Thorsten Liebig, Marko Luther, Ralf Möller, Olaf Noppens, Peter Patel-Schneider, Boontawee Suntisrivaraporn, and Timo Weithöner: DIG 2.0 – Towards a Flexible Interface for Description Logic Reasoners. In Bernardo Cuenca Grau, Pascal Hitzler, Connor Shankey, and Evan Wallace, editors, In Proceedings of the second international workshop OWL: Experiences and Directions, November 2006.

F. Baader, S. Brandt, and C. Lutz: Pushing the EL Envelope. In Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence IJCAI-05. Edinburgh, UK, Morgan-Kaufmann Publishers, 2005.

Sebastian Brandt and Jörg Model: Subsumption in EL w.r.t. hybrid TBoxes. In Proceedings of the 28th Annual German Conference on Artificial Intelligence, KI 2005, in Lecture Notes in Artificial Intelligence. Springer-Verlag, 2005.

Hongkai Liu: Matching in Description Logics with Existential Restrictions and Terminological Cycles. Master thesis, TU Dresden, Germany, 2005.

J. Model: Subsumtion in EL bezüglich hybrider TBoxen. Diploma thesis, TU Dresden, Germany, 2005.

Anni-Yasmin Turhan: Pushing the SONIC border — SONIC 1.0. In Reinhold Letz, editor, FTP 2005 — Fifth International Workshop on First-Order Theorem Proving. Technical Report University of Koblenz, 2005. http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-13-2005.pdf

F. Baader: A Graph-Theoretic Generalization of the Least Common Subsumer and the Most Specific Concept in the Description Logic EL. In J. Hromkovic and M. Nagl, editors, Proceedings of the 30th International Workshop on Graph-Theoretic Concepts in Computer Science (WG 2004), volume 3353 of in Lecture Notes in Computer Science, pages 177–188. Bad Honnef, Germany, Springer-Verlag, 2004.

F. Baader and B. Sertkaya: Applying Formal Concept Analysis to Description Logics. In P. Eklund, editor, Proceedings of the 2nd International Conference on Formal Concept Analysis (ICFCA 2004), volume 2961 of in Lecture Notes in Artificial Intelligence, pages 261–286. Springer, 2004.

F. Baader, B. Sertkaya, and A.-Y. Turhan: Computing the Least Common Subsumer w.r.t. a Background Terminology. In José Júlio Alferes and João Alexandre Leite, editors, Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA 2004), volume 3229 of in Lecture Notes in Computer Science, pages 400–412. Lisbon, Portugal, Springer-Verlag, 2004.

Franz Baader, Baris Sertkaya, and Anni-Yasmin Turhan: Computing the Least Common Subsumer w.r.t. a Background Terminology. In Proceedings of the 2004 International Workshop on Description Logics (DL2004), in CEUR-WS, 2004.

Sebastian Brandt: On Subsumption and Instance Problem in ELH w.r.t. General TBoxes. In Proceedings of the 2004 International Workshop on Description Logics (DL2004), in CEUR-WS, 2004.

Sebastian Brandt: Polynomial Time Reasoning in a Description Logic with Existential Restrictions, GCI Axioms, and—What Else?. In R. López de Mantáras and L. Saitta, editors, Proceedings of the 16th European Conference on Artificial Intelligence (ECAI-2004), pages 298–302. IOS Press, 2004.

Sebastian Brandt and Hongkai Liu: Implementing Matching in ALN. In Proceedings of the KI-2004 Workshop on Applications of Description Logics (KI-ADL'04), in CEUR-WS, September 2004.

Anni-Yasmin Turhan and Christian Kissig: Sonic—Non-standard Inferences go OilEd. In D. Basin and M. Rusinowitch, editors, Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR'04), volume 3097 of in Lecture Notes in Artificial Intelligence. Springer-Verlag, 2004.

Anni-Yasmin Turhan and Christian Kissig: Sonic—System Description. In Proceedings of the 2004 International Workshop on Description Logics (DL2004), in CEUR-WS, 2004.

Franz Baader: Computing the least common subsumer in the description logic EL w.r.t. terminological cycles with descriptive semantics. In Proceedings of the 11th International Conference on Conceptual Structures, ICCS 2003, volume 2746 of in Lecture Notes in Artificial Intelligence, pages 117–130. Springer-Verlag, 2003.

Franz Baader: Least Common Subsumers and Most Specific Concepts in a Description Logic with Existential Restrictions and Terminological Cycles. In Georg Gottlob and Toby Walsh, editors, Proceedings of the 18th International Joint Conference on Artificial Intelligence, pages 319–324. Morgan Kaufman, 2003.

Franz Baader: Terminological Cycles in a Description Logic with Existential Restrictions. In Georg Gottlob and Toby Walsh, editors, Proceedings of the 18th International Joint Conference on Artificial Intelligence, pages 325–330. Morgan Kaufmann, 2003.

Franz Baader: The instance problem and the most specific concept in the description logic EL w.r.t. terminological cycles with descriptive semantics. In Proceedings of the 26th Annual German Conference on Artificial Intelligence, KI 2003, volume 2821 of in Lecture Notes in Artificial Intelligence, pages 64–78. Hamburg, Germany, Springer-Verlag, 2003.

Sebastian Brandt: Implementing Matching in ALE—First Results. In Proceedings of the 2003 International Workshop on Description Logics (DL2003), in CEUR-WS, 2003.

Sebastian Brandt and Anni-Yasmin Turhan: Computing least common subsumers for FLE⁺. In Proceedings of the 2003 International Workshop on Description Logics, in CEUR-WS, 2003.

Sebastian Brandt, Anni-Yasmin Turhan, and Ralf Küsters: Extensions of Non-standard Inferences to Description Logics with transitive Roles. In Moshe Vardi and Andrei Voronkov, editors, Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2003), in Lecture Notes in Computer Science. Springer, 2003.

F. Baader and R. Küsters: Unification in a Description Logic with Inconsistency and Transitive Closure of Roles. In I. Horrocks and S. Tessaris, editors, Proceedings of the 2002 International Workshop on Description Logics, 2002. See http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-53/

F. Baader and A.-Y. Turhan: On the problem of computing small representations of least common subsumers. In Proceedings of the German Conference on Artificial Intelligence, 25th German Conference on Artificial Intelligence (KI 2002), in Lecture Notes in Artificial Intelligence. Aachen, Germany, Springer–Verlag, 2002.

S. Brandt, R. Küsters, and A.-Y. Turhan: Approximating ALCN-Concept Descriptions. In Proceedings of the 2002 International Workshop on Description Logics, 2002.

S. Brandt, R. Küsters, and A.-Y. Turhan: Approximation and Difference in Description Logics. In D. Fensel, F. Giunchiglia, D. McGuiness, and M.-A. Williams, editors, Proceedings of the Eighth International Conference on Principles of Knowledge Representation and Reasoning (KR2002), pages 203–214. San Francisco, CA, Morgan Kaufman, 2002.

S. Brandt and A.-Y. Turhan: An Approach for Optimized Approximation. In Proceedings of the KI-2002 Workshop on Applications of Description Logics (KIDLWS'01), in CEUR-WS. Aachen, Germany, RWTH Aachen, September 2002. Proceedings online available from http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/

F. Baader, S. Brandt, and R. Küsters: Matching under Side Conditions in Description Logics. In B. Nebel, editor, Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI'01, pages 213–218. Seattle, Washington, Morgan Kaufmann, 2001.

F. Baader and P. Narendran: Unification of Concepts Terms in Description Logics. J. Symbolic Computation, 31(3):277–305, 2001.

F. Baader and R. Küsters: Unification in a Description Logic with Transitive Closure of Roles. In R. Nieuwenhuis and A. Voronkov, editors, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001), volume 2250 of in Lecture Notes in Computer Science, pages 217–232. Havana, Cuba, Springer-Verlag, 2001.

F. Baader and A.-Y. Turhan: TBoxes do not yield a compact representation of least common subsumers. In Proceedings of the International Workshop in Description Logics 2001 (DL2001), August 2001.

R. Küsters, and R. Molitor: Approximating most specific concepts in description logics with existential restrictions. In F. Baader, G. Brewka, and T. Eiter, editors, KI 2001: Advances in Artificial Intelligence, Proceedings of the Joint German/Austrian Conference on AI (KI 2001), volume 2174 of Lecture Notes in Artificial Intelligence, pages 217–232. Vienna, Austria, Springer-Verlag, 2001.

R. Küsters and R. Molitor: Computing least common subsumers in ALEN. In B. Nebel, editor, Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI'01, pages 219–224, Seattle, Washington, Morgan Kaufmann, 2001.

A.-Y. Turhan and R. Molitor: Using lazy unfolding for the computation of least common subsumers. In Proceedings of the International Workshop in Description Logics 2001 (DL2001), August 2001.

S. Brandt: Matching under Side Conditions in Description Logics. Diploma thesis, RWTH Aachen, Germany, 2000.

Further Information

DFG Project: Combination of Model and Description Logics 
Principal Investigator: F. Baader 
Involved person: C. Lutz 
Funded by: Deutsche Forschungsgemeinschaft (DFG)

The goal of this project is to establish a direct cooperation between researchers in Modal Logic and researchers in Description Logic in order to achieve a mutual exchange of knowledge and advanced techniques between these two areas. In the one direction, we aim at adapting the strong techniques and meta-results obtained in the area of Modal Logics to Description Logics. In the other direction, we want to use the algorithmic techniques developed in the area of Description Logics to devise implementable algorithms for Modal Logics. Additionally, we investigate the combination of Modal and Description Logics. From the view point of Description Logics, such combinations allow for the representation of intensional knowledge (e.g. about knowledge and belief of intelligent agents) and of dynamic knowledge (e.g. temporal or spatial knowledge). From the view point of Modal Logics, such combinations are fragments of First (or higher) Order Modal Logics which have attractive computational and model-theoretic properties since their first order part is restricted to Description Logics.

This project is a cooperation with Frank Wolter from the University of Leipzig.

Literature:

Franz Baader, Silvio Ghilardi, and Cesare Tinelli: A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Information and Computation, 204(10):1413–1452, 2006.

F. Baader and S. Ghilardi: Connecting Many-Sorted Structures and Theories through Adjoint Functions. In Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS'05), volume 3717 of in Lecture Notes in Artificial Intelligence. Vienna (Austria), Springer-Verlag, 2005.

F. Baader and S. Ghilardi: Connecting Many-Sorted Theories. In Proceedings of the 20th International Conference on Automated Deduction (CADE-05), volume 3632 of in Lecture Notes in Artificial Intelligence, pages 278–294. Tallinn (Estonia), Springer-Verlag, 2005.

Franz Baader and Silvio Ghilardi: Connecting Many-Sorted Theories. LTCS-Report LTCS-05-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. See http://lat.inf.tu-dresden.de/research/reports.html.

F. Baader, S. Ghilardi, and C. Tinelli: A New Combination Procedure for the Word Problem that Generalizes Fusion Decidability Results in Modal Logics. In D. Basin and M. Rusinowitch, editors, Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR'04), volume 3097 of in Lecture Notes in Artificial Intelligence, pages 183–197. Springer-Verlag, 2004.

R. Kontchakov, C. Lutz, F. Wolter, and M. Zakharyaschev: Temporal Tableaux. Studia Logica, 76(1):91–134, 2004.

O. Kutz, C. Lutz, F. Wolter, and M. Zakharyaschev: E-Connections of Abstract Description Systems. Artificial Intelligence, 156(1):1–73, 2004.

F. Baader, R Küsters, and F. Wolter: Extensions to Description Logics. In Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, editors, The Description Logic Handbook: Theory, Implementation, and Applications, pages 219–261. Cambridge University Press, 2003.

Franz Baader, Jan Hladik, Carsten Lutz, and Frank Wolter: From Tableaux to Automata for Description Logics. Fundamenta Informaticae, 57:1–33, 2003.

C. Lutz, F. Wolter, and M. Zakharyaschev: Reasoning about concepts and similarity. In Proceedings of the 2003 International Workshop on Description Logics (DL2003), in CEUR-WS, 2003.

F. Baader, C. Lutz, H. Sturm, and F. Wolter: Fusions of Description Logics and Abstract Description Systems. Journal of Artificial Intelligence Research (JAIR), 16:1–58, 2002.

C. Lutz, H. Sturm, F. Wolter, and M. Zakharyaschev: A Tableau Decision Algorithm for Modalized ALC with Constant Domains. Studia Logica, 72(2):199–232, 2002.

C. Lutz, U. Sattler, and F. Wolter: Description Logics and the Two-Variable Fragment. In D.L. McGuiness, P.F. Pater-Schneider, C. Goble, and R. Möller, editors, Proceedings of the 2001 International Workshop in Description Logics (DL-2001), pages 66–75, 2001. Proceedings online available from http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/

C. Lutz, U. Sattler, and F. Wolter: Modal Logics and the two-variable fragment. In Annual Conference of the European Association for Computer Science Logic CSL'01, in LNCS. Paris, France, Springer Verlag, 2001.

C. Lutz, H. Sturm, F. Wolter, and M. Zakharyaschev: Tableaux for Temporal Description Logic with Constant Domain. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, Proceedings of the International Joint Conference on Automated Reasoning, number 2083 in Lecture Notes in Artifical Intelligence, pages 121–136. Siena, Italy, Springer Verlag, 2001.

F. Baader, C. Lutz, H. Sturm, and F. Wolter: Fusions of Description Logics. In F. Baader and U. Sattler, editors, Proceedings of the International Workshop in Description Logics 2000 (DL2000), number 33 in CEUR-WS, pages 21–30. Aachen, Germany, RWTH Aachen, August 2000. Proceedings online available from http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-33/

C. Lutz and U. Sattler: The Complexity of Reasoning with Boolean Modal Logic. In Advances in Modal Logic 2000 (AiML 2000), 2000. Final version appeared in Advanced in Modal Logic Volume 3, 2001.

Further Information

PhD Project: Non-standard Inference Problems in Description Logics 
Principal Investigator: F. Baader 
Involved person: R. Küsters 
Funded by: Studienstiftung des deutschen Volkes

Literature:

F. Baader, A. Borgida, and D.L. McGuinness: Matching in Description Logics: Preliminary Results. In M.-L. Mugnier and M. Chein, editors, Proceedings of the Sixth International Conference on Conceptual Structures (ICCS-98), volume 1453 of in Lecture Notes in Computer Science, pages 15–34. Montpelier (France), Springer–Verlag, 1998.

F. Baader and P. Narendran: Unification of Concept Terms in Description Logics. In H. Prade, editor, Proceedings of the 13th European Conference on Artificial Intelligence (ECAI-98), pages 331–335. John Wiley & Sons Ltd, 1998.

F. Baader and R. Küsters: Computing the least common subsumer and the most specific concept in the presence of cyclic ALN-concept descriptions. In O. Herzog and A. Günter, editors, Proceedings of the 22nd Annual German Conference on Artificial Intelligence, KI-98, volume 1504 of in Lecture Notes in Computer Science, pages 129–140. Bremen, Germany, Springer–Verlag, 1998.

F. Baader, R. Küsters, and R. Molitor: Structural Subsumption Considered from an Automata Theoretic Point of View. In Proceedings of the 1998 International Workshop on Description Logics DL'98, 1998.

R. Küsters: Characterizing the Semantics of Terminological Cycles in ALN using Finite Automata. In Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR'98), pages 499–510. Morgan Kaufmann, 1998.

PhD Project: Using Novel Inference Services to support the development of models of chemical processes 
Principal Investigator: F. Baader 
Involved person: R. Molitor 
Funded by: DFG Graduiertenkolleg "Informatik und Technik"

In the PhD project Terminological knowledge representation systems in a process engineering application it has been shown that the development of models of chemical processes can be supported by terminological knowledge representation systems. These systems are based on description logics, a highly expressive formalism with well-defined semantics, and provide powerful inference services. The main focus of the project was the investigation of traditional inference services like computing the subsumption hierarchy and instance checking. The new project aims at the formal investigation of novel inference services that allow for a more comprehensive support for the process engineers.

The development of models of chemical processes as carried out at the Department of Process Engineering is based on the usage of so-called building blocks. Using a DL-system, these building blocks can be stored in a class hierarchy. So far, the integration of new (classes of) building blocks into the existing hierarchy is not sufficiently supported. The given system services only allow for checking consistency of extended classes, but they can not be used to define new classes. Hence, the existing classes become larger and larger, the hierarchy degenerates, and the retrieval and re-use of building blocks becomes harder.

The approach considered in this PhD project can be described as follows: instead of directly defining a new class, the knowledge engineer introduces several typical examples (building blocks) of instances of the new class. These examples (resp. their descritpions) are then translated into individuals (resp. concept descriptions) in the DL knowledge base. For the resulting set of concept descriptions, a concept definition describing the examples as specific as possible is automatically computed by computing so-called most specific concepts (msc) and least common subsumers (lcs) (see [1], [2] for detatils). Unfortunately, it turned out that, due to the nature of the algorithms for computing the msc and the lcs and the inherent complexity of these operations, the resulting concept description does not contain defined concepts and is quite large. Thus, in order to obtain a concept description that is easy to read and comprehend, a rewriting of the result is computed [3]. This rewriting is then offered to the knowledge engineer as a possible candidate for the new class definition.

The inference problems underlying the notions most specific concept (msc) and least common subsumer (lcs) were introduced for the DL used in the DL-system Classic developped at AT&T. For DLs relevant in the process engineering application, all novel inference services employed in the approach have been investigated only recently.

Literature:

F. Baader, R. Küsters, and R. Molitor: Computing Least Common Subsumers in Description Logics with Existential Restrictions. In T. Dean, editor, Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI'99), pages 96–101. Morgan Kaufmann, 1999.

F. Baader and R. Molitor: Rewriting Concepts Using Terminologies. In P. Lambrix, A. Borgida, M. Lenzerini, R. Möller, and P. Patel-Schneider, editors, Proceedings of the International Workshop on Description Logics 1999 (DL'99), number 22 in CEUR-WS. Sweden, Linköping University, 1999. Proceedings online available from http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-22/

F. Baader, R. Molitor, and S. Tobies: Tractable and Decidable Fragments of Conceptual Graphs. In W. Cyre and W. Tepfenhart, editors, Proceedings of the Seventh International Conference on Conceptual Structures (ICCS'99), number 1640 in Lecture Notes in Computer Science, pages 480–493. Springer Verlag, 1999.

F. Baader, R. Küsters, and R. Molitor: Structural Subsumption Considered from an Automata Theoretic Point of View. In Proceedings of the 1998 International Workshop on Description Logics DL'98, 1998.

Postgraduate Programme Specification of discrete processes and systems of processes by operational models and logics

The concept of reactive, technical systems forms the motivation for this research project. Such systems can be considered as configurations of resources on which processes, i.e., sequences of actions are running';' such sequences depend on the inner state of the system and on external events. Examples for reactive systems are operating systems, communication systems, control systems of technical installations and systems for medical diagnosis.In our research project we aim at describing processes of such reactive, technical systems by means of formal methods. From these formal descriptions we try to derive properties of all the processes which run on the system. Because of the complexity of such systems, only formal methods can be a sufficient basis for verification and reliability of such properties.There is a huge diversity of formal models for the decription of processes. Roughly, they can be partitioned into operational models and logics. The aim of the research programme is, on the one hand, to continue the investigation about how to describe processes in a formal way and the comparison of different formalizations. On the other hand, we aim at enriching these formal concepts by verification techniques.

Further Information

EU-LTR Project: Data Warehouse Quality (DWQ) 
Principal Investigator: F. Baader 
Involved person: U. Sattler 
Funded by: EU

Due to the increasing speed and memory capacities of information systems, the amount of data processed by these systems is steadily increasing. Furthermore, the data available in electronic form is increasing tremendously, too. As a consequence, enterprises can access a huge amount of data concerning their business. Unfortunately, these data is mostly distributed among different systems and thus has different formats and thus cannot be consolidated as a whole. Now, data warehouses are designed to process these huge amounts of data in such a way that decisions can be based on this data. Data warehouses are software tools closely related to database systems which have the following features: They allow (1) to extract and integrate data from different sources into a central schema, (2) to combine and aggregate this integrated data, and (3) to ask ad-hoc queries. Furthermore, they are closely related to "on-line analytical processing"-systems (OLAP) and "decision-support-systems" (DSS).

Within the DWQ project, we are mainly concerned with the investigation of multidimensional aggregation. This comprises aggregation and part-whole relations per se as well as properties of multiply hierarchically structured domains such as time, space, organizations, etc. The understanding of these properties shall lead to a formalism that supports the aggregation of information along multiple dimensions. The degree of support will be evaluated with respect to the quality criteria developed within this project.

Literature:

I. Horrocks and U. Sattler: A Description Logic with Transitive and Inverse Roles and Role Hierarchies. Journal of Logic and Computation, 9(3):385–410, 1999.

F. Baader and U. Sattler: Description Logics with Concrete Domains and Aggregation. In H. Prade, editor, Proceedings of the 13th European Conference on Artificial Intelligence (ECAI-98), pages 336–340. John Wiley & Sons Ltd, 1998.

I. Horrocks and U. Sattler: A Description Logic with Transitive and Converse Roles and Role Hierarchies. In Proceedings of the International Workshop on Description Logics. Povo - Trento, Italy, IRST, 1998.

F. Baader and U. Sattler: Description Logics with Aggregates and Concrete Domains. In Proceedings of the International Workshop on Description Logics, 1997.

Project: Design of a Medical Information System with Vague Knowledge 
Principal Investigator: F. Baader 
Involved person: C. Tresp 
Funded by: DFG Graduiertenkolleg "Informatik und Technik"

Literature:

R. Molitor and C.B. Tresp: Extending Description Logics to Vague Knowledge in Medicine. In P. Szczepaniak, P.J.G. Lisboa, and S. Tsumoto, editors, Fuzzy Systems in Medicine, volume 41 of in Studies in Fuzziness and Soft Computing, pages 617–635. Springer Verlag, 2000.

C.B. Tresp and R. Molitor: A Description Logic for Vague Knowledge. In Proceedings of the 13th biennial European Conference on Artificial Intelligence (ECAI'98), pages 361–365. Brighton, UK, J. Wiley and Sons, 1998.

C. Tresp and U. Tüben: Medical Terminology Processing for a Tutoring System. In International Conference on Computational Intelligence and Multimedia Applications (ICCIMA98), Februar 1998.

J. Weidemann, H.-P. Hohn, J. Hiltner, K. Tochtermann, C. Tresp, D. Bozinov, K. Venjakob, A. Freund, B. Reusch, and H.-W. Denker: A Hypermedia Tutorial for Cross-Sectional Anatomy: HyperMed. Acta Anatomica, 158, 1997.

Project: On the expressive power of loop constructs in imperative programming languages 
Involved persons: K. Indermark, C. A. Albayrak

Literature:

Can Adam Albayrak and Thomas Noll: The WHILE Hierarchy of Program Schemes is Infinite. In Maurice Nivat, editor, Proceedings of Foundations of Software Science and Computation Structures, pages 35–47. LNCS 1378, Springer, 1998.

C.A. Albayrak: Die WHILE-Hierarchie für Programmschemata. RWTH Aachen, 1998.

Project: Using Novel Inference Services to support the development of models of chemical processes 
Principal Investigator: F. Baader 
Involved person: U. Sattler 
Funded by: DFG Graduiertenkolleg "Informatik und Technik"

In this project, the suitability of different terminological KR languages for representing relevant concepts in different engineering domains will be investigated. In cooperation with Prof. Dr. Marquardt, Aachen, we are trying to design a terminological KR language that is expressive enough to support modeling in process engineering, without having inference problems of unacceptably high complexity. The goal of representing this knowledge is to support the modeling of large chemical plants for planing and optimization purposes. The complex structure of such plants demands for a highly expressive terminological language, in particular because the support of top-down modeling requires the appropriate treatment of part-whole relations. The formally well-founded and algorithmically manageable integration of such relations is one of our main research goals here.

Literature:

U. Sattler: Terminological knowledge representation systems in a process engineering application. LuFG Theoretical Computer Science, RWTH-Aachen, 1998.

F. Baader and U. Sattler: Description Logics with Symbolic Number Restrictions. In W. Wahlster, editor, Proceedings of the Twelfth European Conference on Artificial Intelligence (ECAI-96), pages 283–287. John Wiley & Sons Ltd, 1996. An extended version has appeared as Technical Report LTCS-96-03

F. Baader and U. Sattler: Knowledge Representation in Process Engineering. In Proceedings of the International Workshop on Description Logics. Cambridge (Boston), MA, U.S.A., AAAI Press/The MIT Press, 1996.

F. Baader and U. Sattler: Number Restrictions on Complex Roles in Description Logics. In Proceedings of the Fifth International Conference on the Principles of Knowledge Representation and Reasoning (KR-96). Morgan Kaufmann, Los Altos, 1996. An extended version has appeared as Technical Report LTCS-96-02

U. Sattler: A Concept Language Extended with Different Kinds of Transitive Roles. In G. Görz and S. Hölldobler, editors, 20. Deutsche Jahrestagung für Künstliche Intelligenz, number 1137 in Lecture Notes in Artificial Intelligence. Springer Verlag, 1996.

Project: Integration of modal operators into terminological knowledge representation languages 
Involved persons: F. Baader in cooperation with Deutsches Forschungszentrum für Künstliche Intelligenz (DFKI) andMax-Planck-Institut für Informatik (MPI)

Traditional terminological knowledge representation systems can be used to represent the objective, time-independent knowledge of an application domain. Representing subjective knowledge (e.g., belief and knowledge of intelligent agents) and time-dependent knowledge is only possible in a very restricted way. In systems modeling aspects of intelligent agents, however, intentions, beliefs, and time-dependent facts play an important role.

Modal logics with Kripke-style possible worlds semantics yields a formally well-founded and well-investigated framework for the representation of such notions. However, most modal logics have been defined using first order predicate logic as underlying formalism. This leads to strong undecidability of these logics. Substituting first order predicate logic by terminological languages as underlying formalism, one might substantially raise the expressive power of the terminological language while preserving the decidability of the inference problems.

In collaboration with researchers at DFKI and MPII (Saarbrücken), we are investigating different possibilities for integrating modal operators into terminological KR systems. Our main goal is to design a combined formalism for which all the important terminological inference problems (such as the subsumption problem) are still decidable. Otherwise, it would not be possible to employ such a formalism in an implemented system.

Literature:

F. Baader and A. Laux: Terminological Logics with Modal Operators. In C. Mellish, editor, Proceedings of the 14th International Joint Conference on Artificial Intelligence, pages 808–814. Montréal, Canada, Morgan Kaufmann, 1995.

F. Baader and H.-J. Ohlbach: A Multi-Dimensional Terminological Knowledge Representation Language. J. Applied Non-Classical Logics, 5:153–197, 1995.

H.-J. Ohlbach and F. Baader: A Multi-Dimensional Terminological Knowledge Representation Language. In Proceedings of the 13th International Joint Conference on Artificial Intelligence, IJCAI-93, pages 690–695, 1993.

DFG Project: Combination of special deduction procedures 
Principal Investigator: F. Baader 
Involved person: J. Richts 
Funded by: DFG, Schwerpunkt "Deduktion"

Since September 1994, this research project is funded within the Schwerpunkt "Deduktion" by the Deutsche Forschungsgemeinschaft (DFG) for two years, possibly with a prolongation for two more years. It is joint work with the research group of Prof. Schulz at the CIS, University of Munich.

This research is mainly concerned with combining decision procedures for unification problems. Such a procedure can be used to decide whether a given set of equations is solvable with respect to an equational theory or a combination of equational theories. For unification procedures that return complete sets of unifiers, the combination problem has been investigated in greater detail. In contrast to these procedures, a decision procedure only returns a boolean value as result indicating whether a solution exists or not.

One aim of this research project is to develop optimizations of the known combination method for decision procedures, which apply to restricted classes of equational theories. The general combination algorithm is nondeterministic, which means that in the worst-case, exponentially many possibilities must be investigated. If the equational theories under consideration satisfy some simple syntactic restrictions, large parts of the search tree can be pruned. We will investigate to which extent such optimizations are possible.

Another aim is to generalize the existing combination algorithms, for instance to the case of theories with non-disjoint signatures, or to more general problems than unification problems. The long-term objective of this research is to reach a better understanding of the basic algorithmic problems that occur when combining special deduction procedures, and to develop a rather general combination framework.

Since many optimized combination algorithms depend on special procedures that satisfy additional requirements, we will also investigate how well-known special inference procedures can be extended in this direction.

In order to be able to assess the effects of our optimizations and to determine their relevance in practice, we will implement the investigated unification algorithms - the combination algorithm as well as selected special algorithms. For the implementation of special unification algorithms, we have chosen the equational theories A, AC and ACI, which contain a binary function symbol that is associative, commutative, and/or idempotent.

Literature:

Stephan Kepser and Jörn Richts: Optimisation Techniques for Combining Constraint Solvers. In Dov Gabbay and Maarten de Rijke, editors, Frontiers of Combining Systems 2, Papers presented at FroCoS'98, pages 193–210. Amsterdam, Research Studies Press/Wiley, 1999.

Stephan Kepser and Jörn Richts: UniMoK: A System for Combining Equational Unification Algorithms. In Rewriting Techniques and Applications, Proceedings RTA-99, volume 1631 of in Lecture Notes in Computer Science, pages 248–251. Springer-Verlag, 1999.

Jörn Richts: Effiziente Entscheidungsverfahren zur E-Unifikation. PhD Thesis, RWTH Aachen. Shaker Verlag, Germany, 1999.

F. Baader and K. Schulz: Combination of Constraint Solvers for Free and Quasi-Free Structures. Theoretical Computer Science, 192:107–161, 1998.

F. Baader and C. Tinelli: Deciding the Word Problem in the Union of Equational Theories. UIUCDCS-Report UIUCDCS-R-98-2073, Department of Computer Science, University of Illinois at Urbana-Champaign, 1998.

F. Baader: Combination of Compatible Reduction Orderings that are Total on Ground Terms. In G. Winskel, editor, Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS-97), pages 2–13. Warsaw, Poland, IEEE Computer Society Press, 1997.

F. Baader and C. Tinelli: A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method. In W. McCune, editor, Proceedings of the 14th International Conference on Automated Deduction (CADE-97), volume 1249 of in Lecture Notes in Artificial Intelligence, pages 19–33. Springer-Verlag, 1997.

Franz Baader and Klaus U. Schulz, editors: Frontiers of Combining Systems. Kluwer Academic Publishers, 1996.

F. Baader and K. U. Schulz: Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. J. Symbolic Computation, 21:211–243, 1996.

Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, and Jörg Siekmann: Die Beweisentwicklungsumgebung Omega-MKRP. Informatik – Forschung und Entwicklung, 11(1):20–26, 1996. In German

F. Baader and K.U. Schulz: Combination Techniques and Decision Problems for Disunification. Theoretical Computer Science B, 142:229–255, 1995.

F. Baader and K.U. Schulz: Combination of Constraint Solving Techniques: An Algebraic Point of View. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of in Lecture Notes in Artificial Intelligence, pages 352–366. Kaiserslautern, Germany, Springer Verlag, 1995.

F. Baader and K.U. Schulz: On the Combination of Symbolic Constraints, Solution Domains, and Constraint Solvers. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, CP95, volume 976 of in Lecture Notes in Artificial Intelligence, pages 380–397. Cassis, France, Springer Verlag, 1995.

Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, and Jörg Siekmann: KEIM: A Toolkit for Automated Deduction. In Alan Bundy, editor, Automated Deduction — CADE-12, in Proceedings of the 12th International Conference on Automated Deduction, pages 807–810. Nancy, Springer-Verlag LNAI 814, 1994.

F. Baader and K. Schulz: Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. In Proceedings of the 11th International Conference on Automated Deduction, CADE-92, volume 607 of in Lecture Notes in Computer Science, pages 50–65. Saratoga Springs (USA), Springer–Verlag, 1992.