Chair of Automata Theory at the Institute of Theoretical Computer Science of the Faculty of Computer Science of the Technische Universität Dresden

Research Activities

Current Research Projects

Completed Research Projects


Details about the Research Activities

Most of the research done in our group is concerned with automated deduction, that is, with the problem of how to automate the process of drawing logical inferences. In this context, we are mainly interested in subclasses of first-order predicate logic for which the interesting inference problems are still decidable. On one hand, we are investigating the combination of special deduction methods, and their integration into general deduction procedures. On the other hand, we are designing logic-based knowledge representation languages with decidable inference problems.


Deduction

Within the research area of deduction we are interested in automatic theorem proving, term rewriting, and unification.

In particular, we turned our attention to the integration of special deduction methods (see completed research project Combination of Specific Deduction Procedures): When solving logical inference problems, one can choose between two fundamentally different ways of proceeding. On one hand, one can try to design special inferences methods that are tailored to a particular class of inference problems. These methods are usually rather efficient, but they only apply to the restricted class they have been designed for. On the other hand, one can try to apply general purpose deduction procedures (such as resolution-based theorem proving or Knuth-Bendix completion). The integration of special inference methods into general purpose deductive systems aims at a combination of the efficiency of the special method with the universality of the general method. In this context, one is faced with the problems of how to combine a special inference method with a general purpose inference procedure, and of how to combine different special inference methods with each other. Combination problems of the second kind have already been investigated in depth for the combination of algorithm for unification modulo equational theories over disjoint signatures.


Knowledge representation

Terminological knowledge representation (KR) languages have been developed as a structured formalisms for representing of the taxonomic knowledge of a given application domain. Terminological knowledge representation systems are, for example, applied in natural language processing, in automated planning systems, and for supporting configuration of technical systems. An important point in favour of terminological KR languages is that they are equipped with a clear and formally well-understood logic-based semantics.

On one hand, this formalization shows that terminological KR languages can be viewed as subclasses of first order predicate logic. From an algorithmic point of view it is important that many of the languages considered until now yield decidable subclasses of first order predicate logic, which are not contained in one of the well-known decidable fragments. For these languages, decision procedures have been developed that are based on the well-known tableaux calculus for predicate logic. Interestingly, this approach usually yields procedures that are optimal with respect to worst case complexity of the respective inference problem.

On the other hand, the formal semantics provides us with an implementation-independent description of the behaviour of a terminological system. This improves the transparency for the user of such a system, and it facilitates comparing different systems.


Computing with Molecules

Dr. Monika Sturm
Dr. Thomas Hinze

Different ideas for development of unconventional models for computation were discussed and realized during the last years. Some of these developments are based on abstractions of molecular biological processes (e.g. recombination) for application in mathematics and computer science. The resulting models for computation supplement their classical counterparts from theoretical computer science. Molecules of DNA (deoxyribonucleic acid) serve as data carrier and as storage medium for information. Suitable molecular biological reactions and processes on DNA are used as operations. Research activities aim to construct a model for a universal biological computer that can be implemented in a molecular biological laboratory. Algorithms for biological computers particularly feature by massive data parallelism and high computational speed leading to a challenge for the electronic state of the art technology. Research topics:


Current Research Projects


A Logic of Aggregation and Emerging Functionality

Project: A Logic of Aggregation and Emerging Functionality
Principal Investigator:
F. Baader
Involved person: D. Walther
Start date: January 1, 2013
Duration years: 3 years
Funded by: DFG Cluster of Excellence Center for Advancing Electronics Dresden (cfAED)

In biological systems, large entities can be described as an aggregation of smaller components. However, such a description ignores a wide range of functionalities that emerge as a consequence of the aggregation of the smaller parts. For example, while tissues are composed of many cells with a common behaviour, it is also true that damaging or even killing some of the cells in a tissue does not disrupt the activities in the tissue itself; that is, a new functionality (resilience to damage) emerged from the combination of parts that did not have the functionality themselves.

The aim of this project is to develop a logic-based modelling language that is expressive enough to describe such emerging phenomena, but still allows effective reasoning. The development of the formalism will be guided and motivated by examples found in biological systems. The approach will consist on identifying the properties of the emerging phenomena of interests for biology, and generalize them to a formal description language.

To evaluate the resulting formalism, we will compare it to known models developed in systems biology in terms of expressivity, modularity and prediction capabilities.

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


Extraction of General Concept Inclusions with Confidence from Models

PhD Project: Extraction of General Concept Inclusions with Confidence from Models
Principal Investigators:
F. Baader, B. Ganter G. Brewka
Involved person: B. Borchmann
Start date: October 1, 2012
Duration: 3 years
Funded by: DFG Research Training Group Quantitative Logics and Automata (QuantLA)

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


Quantitative methods for similarity and generalization in Description Logics

PhD Project: Quantitative methods for similarity and generalization in Description Logics
Principal Investigators:
F. Baader, C. Baier, A.-Y. Turhan,
Involved person: A. Ecke
Start date: October 1, 2012
Duration: 3 years
Funded by: DFG Research Training Group Quantitative Logics and Automata (QuantLA)

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


Verification of Non-Terminating Action Programs

Project: Verification of Non-Terminating Action Programs
Principal Investigators:
F. Baader, G. Lakemeyer
Involved person: B. Zarrieß
Start date: July 1, 2012
Duration: 3 years
Funded by: DFG Research Unit Hybrid Reasoning for Intelligent Systems (HYBRIS)

The action language GOLOG has been used, among other things, for the specification of the behaviour of mobile robots. Since the task of such autonomous systems is typically open-ended, their GOLOG programs are usually non-terminating. To ensure that the program will let the robot exhibit the intended behaviour, it is often desirable to be able to formally specify and then verify the desired properties, which are often of a temporal nature. This task has been studied within our preliminary work from two perspectives: On the one hand, the problem was tackled for very expressive specification and action program formalisms, but without the goal of achieving decidability, i.e. the developed verification methods were not guaranteed to terminate. On the other hand, the verification problem was studied for action formalisms based on decidable description logics and very limited means of specifying admissible sequences of actions, which allowed us to show decidability and complexity results for the verification problem. The purpose of this project is to combine the advantages of both approaches by, on one hand, developing verification methods for GOLOG programs that are effective and practically feasible and, on the other hand, going beyond the formalisms with very limited expressiveness to enhance their usefulness. Among other things, both qualitative and quantitative temporal program properties will be addressed.

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


Reasoning in Fuzzy Description Logics with General Concept Inclusion Axioms

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.


Automatic Generation of Description Logic-based Biomedical Ontologies

Project: Automatic Generation of Description Logic-based Biomedical Ontologies
Principal Investigators:
F. Baader, M. Schroeder
Involved person: Y. Ma
Start date: April 1, 2012
Duration: 3 years
Funded by: DFG Research Unit Hybrid Reasoning for Intelligent Systems (HYBRIS)

Ontologies such as the Gene Ontology and SNOMED CT play a major role in biology and medicine since they facilitate data integration and the consistent exchange of information between different entities. They can also be used to index and annotate data and literature, thus enabling efficient search and analysis. Unfortunately, creating the required ontologies manually is a complex, error-prone, and time and personnel-consuming effort. For this reason, approaches that try to learn ontologies automatically from text and data have been developed. The ontologies generated by these approaches are, however, usually not formal ontologies, i.e., the concepts learned by these approaches are not equipped with a formal definition. The goal of this project is to combine the expertise in ontology learning from text of Prof. Schroeder’s group with the Description Logic expertise of Prof. Baader’s group in order to develop approaches for learning Description Logic-based ontologies from text and data. The main idea is to apply non-standard Description Logic inferences developed in Prof. Baader’s group to the result of the ontology learning approach developed in Prof. Schroeder’s group in order to generate concept definitions and additional constraints (general concept inclusions). The envisioned approach is hybrid since the non-standard inferences will be modified such that they can take into account numerical information on the quality of the results produced by the ontology learning approaches.

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


Semantic Technology for Context Awareness

Project: Semantic Technology for Context Awareness
Principal Investigator:
F. Baader
Involved persons: Eldora, S. Borgwardt, V. Thost
Start date: July 1, 2011
Duration: 4 years
Funded by: DFG Collaborative Research Centre Highly Adaptive Energy-Efficient Computing (HAEC)

The main challenge addressed in this project is how to represent context information relevant for enhancing energy efficiency in a formally well-founded way, and how to integrate different context information into a coherent semantic view. To address this challenge, we will employ ontologies expressed in appropriate decidable, logic-based ontology languages. Rather than content ourselves with using existing ontology languages such as OWL, which were designed for other purposes, we will develop new ones that are tailored towards representing context information relevant for enhancing energy efficiency.

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


Temporalised Description Logics with Good Algorithmic Properties, and Their Application for Monitoring Partially Observable Events

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.


Unification in Description Logics for Avoiding Redundancies in Medical Ontologies

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.


Completed Research Projects


Completing knowledge bases using Formal Concept Analysis

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.


Knowledge Acquisition in Description Logics by Means of Formal Concept Analysis

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.


Description Logics with Existential Quantifiers and Polynomial Subsumption Problem and Their Applications in Bio-Medical Ontologies

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 ELHIfR+. 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 ELHIfR+. 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.


Action Formalisms with Description Logic

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.


TONES

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:

Explaining Ontology Consequences

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.


Novel Inference Services in Description Logics

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.


Logic Algorithms in Knowledge Representation

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 C2. 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.


Combination of Modal and Description Logics

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.


Multidimensional aggregation

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.


Non-standard Inference Problems in Description Logics

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.


Using Novel Inference Services to support the development of models of chemical processes

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.


Integration of modal operators into terminological knowledge representation languages

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) and Max-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.


On the expressive power of loop constructs in imperative programming languages

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.


Combination of special deduction procedures

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.


Terminological knowledge representation for supporting modeling in an engineering application

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.


Design of a Medical Information System with Vague Knowledge

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.


Back to the hompage of the Chair of Automata Theory.