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.
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.
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.
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:
DFG Project: Completing knowledge bases using Formal Concept Analysis
Principal Investigator: F. Baader
Involved persons: B. Sertkaya
Start date: November 15th, 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.
Publications on the topics of this project can be found on our publications web page.
PhD Project: Knowledge Acquisition in Description Logics by Means of Formal Concept Analysis
Principal Investigator: F. Baader
Involved persons: F. Distel
Start date: May 1st, 2007
Duration: 2 years
Funded by: Cusanuswerk e.V.
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.
Publications on the topics of this project can be found on our publications web page.
DFG Project: Explaining Ontology Consequences
Principal Investigator: F. Baader
Involved persons: R. Penaloza
Start date: April 1th, 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.
Publications on the topics of this project can be found on our publications web page.
DFG Project: Description Logics with Existential Quantifiers and Polynomial Subsumption Problem and Their Applications in Bio-Medical Ontologies
Principal Investigator: F. Baader
Involved persons: C. Lutz, B. Suntisrivaraporn.
Start date: June 1st, 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.
Publications on the topics of this project can be found on our publications web page.
DFG Project: Action Formalisms with Description Logic
Principal Investigator: F. Baader, M. Thielscher.
Involved persons: C. Drescher, H. Liu, C. Lutz, M. Milicic.
Start date: September 1st, 2005
Duration: 2 years + 2-year-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.
Publications on the topics of this project can be found on our publications web page.
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 1st, 2005
Duration: 36 Months
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.
Publications on the topics of this project can be found on our publications web page.
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.F. Baader, S. Brandt, A. -Y. Turhan,
DFG Project: Novel Inference Services in Description Logics
Literature:
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, 2001. Morgan Kaufmann.
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 Lecture Notes in Computer Science, pages 217–232, Havana, Cuba, 2001. Springer-Verlag.
F. Baader and P. Narendran. Unification of Concepts Terms in Description Logics. J. Symbolic Computation, 31(3):277–305, 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), Stanford, USA, August 2001.
S. Brandt. Matching under Side Conditions in Description Logics. Diploma thesis, RWTH Aachen, Germany, 2000.
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, 2002. Morgan Kaufman.
S. Brandt and A.-Y. Turhan. Using Non-standard Inferences in Description Logics—what does it buy me?. In Proceedings of the KI-2001 Workshop on Applications of Description Logics (KIDLWS'01), number 44 in CEUR-WS, Vienna, Austria, September 2001. RWTH Aachen.
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, 2001. Springer-Verlag.
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, 2001. Morgan Kaufmann.
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), Stanford, USA, August 2001.
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 Lecture Notes in Artificial Intelligence, pages 117–130. Springer-Verlag, 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 Lecture Notes in Artificial Intelligence, pages 64–78, Hamburg, Germany, 2003. Springer-Verlag.
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.
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 Lecture Notes in Computer Science, pages 177–188, Bad Honnef, Germany, 2004. Springer-Verlag.
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, 2005. Morgan-Kaufmann Publishers.
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, Toulouse, France, 2002. See http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-53/.
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 International Mathematical Series, pages 1–75. Springer-Verlag, 2006.
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 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 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 Lecture Notes in Computer Science, pages 400–412, Lisbon, Portugal, 2004. Springer-Verlag.
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), CEUR-WS, 2004.
Franz Baader, Baris 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.-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), Lecture Notes in Artificial Intelligence, Aachen, Germany, 2002. Springer–Verlag.
Sebastian Brandt. Implementing Matching in ALE—First Results. In Proceedings of the 2003 International Workshop on Description Logics (DL2003), CEUR-WS, 2003.
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), 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. Standard and Non-standard Reasoning in Description Logics. Ph.D. dissertation, Institute for Theoretical Computer Science, TU Dresden, Germany, 2006.
S. Brandt, R. Küsters, and A.-Y. Turhan. Approximating ALCN-Concept Descriptions. In Proceedings of the 2002 International Workshop on Description Logics, 2002.
Sebastian Brandt and Hongkai Liu. Implementing Matching in ALN. In Proceedings of the KI-2004 Workshop on Applications of Description Logics (KI-ADL'04), CEUR-WS, Ulm, Germany, September 2004.
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, Lecture Notes in Artificial Intelligence. Springer-Verlag, 2005.
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), CEUR-WS, Aachen, Germany, September 2002. RWTH Aachen. Proceedings online available from http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/.
Sebastian Brandt and Anni-Yasmin Turhan. Computing least common subsumers for FLE^+. In Proceedings of the 2003 International Workshop on Description Logics, 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), Lecture Notes in Computer Science. Springer, 2003.
Hongkai Liu. Matching in Description Logics with Existential Restrictions and Terminological Cycles. Master's thesis, Dresden University of Technology, Germany, 2005.
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.
J. Model. Subsumtion in EL bezüglich hybrider TBoxen. Diploma thesis, TU Dresden, Germany, 2005.
Baris 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, 2006. Verlag Allgemeine Wissenschaft.
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.
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.
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 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), CEUR-WS, 2004.
Project summaryF. Baader, S. Tobies, J. Hladik
DFG Projekt: Logik-Algorithmen in der Wissensrepräsentation
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:
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 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 Lecture Notes in Artificial Intelligence, pages 1–18, St Andrews, Scotland, UK, 2000. Springer-Verlag.
C. Hirsch and S. Tobies. A Tableau Algorithm for the Clique Guarded Fragment. In Proceedings of the Workshop Advances in Modal Logic AiML 2000, Leipzig, Germany, 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), Aachen, Germany, 2000.
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.
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.
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.
I. Horrocks, U. Sattler, and S. Tobies. Practical Reasoning for Very Expressive Description Logics. Logic Journal of the IGPL, 8(3):239–264, May 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, 2000. Springer Verlag.
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, 2000. Morgan Kaufmann Publishers.
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, July 30 – August 1 1999. Linköping University.
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.
S .Tobies. A NExpTime-complete Description Logic Strictly Contained in C^2. In J. Flum and M. Rodríguez-Artalejo, editors, Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL-99), 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, LNAI 1632, pages 52–66, Trento, Italy, July 7–10, 1999. Springer-Verlag.
Stephan Tobies. The Complexity of Reasoning with Cardinality Restrictions and Nominals in Expressive Description Logics. Journal of Artificial Intelligence Research, 12:199–217, May 2000.
Stephan Tobies. PSPACE Reasoning for Graded Modal Logics. Journal of Logic and Computation, 11(1):85–106, 2001.
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 Lecture Notes in Artificial Intelligence, pages 92–106. Springer-Verlag, 2001.
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 Lecture Notes in Computer Science, pages 1–32. Springer, 2003.
F. Baader, J. Hladik, C. Lutz, and F. Wolter. From Tableaux to Automata for Description Logics. Fundamenta Informaticae, 57:1–33, 2003.
J. Hladik. Implementierung eines Entscheidungsverfahrens für das Bewachte Fragment der Prädikatenlogik. Diploma thesis, RWTH Aachen, Germany, 2001.
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 Lecture Notes in Artificial Intelligence. Springer-Verlag, 2002.
Jan Hladik. Reasoning about Nominals with FaCT and RACER. In Proceedings of the 2003 International Workshop on Description Logics (DL2003), CEUR-WS, 2003.
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. DFKI, 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.
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 Lecture Notes in Artificial Intelligence. Springer Verlag, 2003.
J. Hladik. A Tableau System for the Description Logic SHIO. In Ulrike Sattler, editor, Contributions to the Doctoral Programme of IJCAR 2004. CEUR, 2004.
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 Lecture Notes in Artificial Intelligence. Springer Verlag, 2002.
S. Tobies. Complexity Results and Practical Algorithms for Logics in Knowledge Representation. PhD thesis, RWTH Aachen, 2001.
F. Baader, C. Lutz
DFG Project: Combination of Modal and Description Logics
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:
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.
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 and U. Sattler. The Complexity of Reasoning with Boolean Modal Logic. In Advances in Modal Logic 2000 (AiML 2000), Leipzig, Germany, 2000. Final version appeared in Advanced in Modal Logic Volume 3, 2001.
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, LNCS, Paris, France, 2001. Springer Verlag.
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, Stanford, California, USA, 2001.
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 Lecture Notes in Artificial Intelligence, Vienna (Austria), 2005. Springer-Verlag.
F. Baader and S. Ghilardi. Connecting Many-Sorted Theories. In Proceedings of the 20th International Conference on Automated Deduction (CADE-05), volume 3632 of Lecture Notes in Artificial Intelligence, pages 278–294, Tallinn (Estonia), 2005. Springer-Verlag.
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), Lecture Notes in Artificial Intelligence. Springer-Verlag, 2004.
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.
Franz Baader, Jan Hladik, Carsten Lutz, and Frank Wolter. From Tableaux to Automata for Description Logics. Fundamenta Informaticae, 57:1–33, 2003.
Franz Baader and Silvio Ghilardi. Connecting Many-Sorted Theories. LTCS-Report 05-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.
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.
C. Lutz, F. Wolter, and M. Zakharyaschev. Reasoning about concepts and similarity. In Proceedings of the 2003 International Workshop on Description Logics (DL2003), CEUR-WS, 2003.
F. Baader, C. Lutz, H. Sturm, and F. Wolter. Fusions of Description Logics. In Proceedings of the International Workshop in Description Logics 2000, number 33 in CEUR-WS, pages 21-30, Aachen, Germany, August 2000.
C. Lutz, H. Sturm, F. Wolter, and M. Zakharyaschev. Tableaux for Temporal Description Logic with Constant Domain. In Proceedings of the International Joint Conference on Automated Reasoning, Siena, Italy, 2001.
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.
F. Baader, U. Sattler
EU-LTR-Project Data Warehouse Quality (DWQ)
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:
F. Baader, 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, U. Sattler: A Description Logic with Transitive and Inverse Roles and Role Hierarchies . To appear in the Journal of Logic and Computation, 1998.
I. Horrocks, 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, 1999. IRST.
F. Baader, U. Sattler: Description Logics with Aggregates and Concrete Domains . In Proceedings of the International Workshop on Description Logics, Gif sur Yvette, France, 1997.
F. Baader, R. Küsters
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 Lecture Notes in Computer Science, pages 15-34, Montpelier (France), 1998. Springer-Verlag.
F. Baader, 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 Lecture Notes in Computer Science, pages 129-140, Bremen, Germany, 1998. Springer-Verlag.
F. Baader, R. Küsters, R. Molitor: Structural Subsumption Considered from an Automata Theoretic Point of View . In Proceedings of the 1998 International Workshop on Description Logics DL'98, Trento, Italy, 1998.
F. Baader, 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.
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.
F. Baader, R. Molitor
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, R. Molitor: Structural Subsumption Considered from an Automata Theoretic Point of View . In Proceedings of the 1998 International Workshop on Description Logics DL'98, Trento, Italy, 1998.
F. Baader, R. Molitor, R. Küsters: Computing Least Common Subsumer in Description Logics with Existential Restrictions. In Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI'99).
F. Baader, R. Molitor, S. Tobies: Tractable and Decidable Fragments of Conceptual Graphs. In Proceedings of the Seventh International Conference on Conceptual Structures (ICCS'99), Lecture Notes in Computer Science. Springer Verlag.
F. Baader, R. Molitor: Rewriting Concepts using Terminologies. In Proceedings of the International Workshop on Description Logics 1999 (DL'99).
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, H.-J. Ohlbach: A Multi-Dimensional Terminological Knowledge Representation Language. In Proceedings of the 13th International Joint Conference on Artificial Intelligence, IJCAI-93.
F. Baader, A. Laux: Terminological Logics with Modal Operators. In C. Mellish, editor, Proceedings of the 14th International Joint Conference on Artificial Intelligence.
F. Baader, H.-J. Ohlbach: A Multi-Dimensional Terminological Knowledge Representation Language. J. Applied Non-Classical Logics, 5:153-197, 1995.
K. Indermark, C.A. Albayrak
Literature:
C.A. Albayrak, T. 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 . PhD thesis, RWTH Aachen, 1998.
F. Baader, J. Richts
Schwerpunkt "Deduktion" of the DFG
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:
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, 1997. IEEE Computer Society Press.
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 Lecture Notes in Computer Science, pages 50–65, Saratoga Springs (USA), 1992. Springer–Verlag.
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 Lecture Notes in Artificial Intelligence, pages 352–366, Kaiserslautern, Germany, 1995. Springer Verlag.
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. 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 Lecture Notes in Artificial Intelligence, pages 380–397, Cassis, France, 1995. Springer Verlag.
Franz Baader and Klaus U. Schulz, editors. Frontiers of Combining Systems. Proceedings of First International Workshop, Applied Logic Series 3. 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.
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. 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 Lecture Notes in Artificial Intelligence, pages 19–33. Springer-Verlag, 1997.
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.
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, 1999. Research Studies Press/Wiley.
Jörn Richts. Effiziente Entscheidungsverfahren zur E-Unifikation. Dissertation an der RWTH Aachen. Shaker Verag, Germany
X. Huang, M. Kerber, M. Kohlhase, E. Melis, D. Nesmith, J. Richts, J. Siekmann: KEIM: A Toolkit for Automated Deduction . In Alan Bundy, editor, Automated Deduction - CADE-12, Proceedings of the 12th International Conference on Automated Deduction, pages 807-810, Nancy, 1994. Springer-Verlag LNAI 814.
X. Huang, M. Kerber, M. Kohlhase, E. Melis, D. Nesmith, J. Richts, J. Siekmann: Die Beweisentwicklungsumgebung Omega-MKRP. Informatik - Forschung und Entwicklung, 11(1):20-26, 1996. In German.
S. Kepser, J. Richts: A System for Combining Equational Unification Algorithms . Submitted, 1999.
F. Baader, U. Sattler
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 . PhD thesis, RWTH-Aachen, 1998.
F. Baader, 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.
F. Baader, U. Sattler: Knowledge Representation in Process Engineering . In Proceedings of the International Workshop on Description Logics, Cambridge (Boston), MA, U.S.A., 1996. AAAI Press/The MIT Press.
F. Baader, 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.
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, Nummer 1137 der Lecture Notes in Artificial Intelligence. Springer Verlag, 1996.
F. Baader, C. Tresp
DFG Graduiertenkolleg "Informatik und Technik"
Literature:
J. Weidemann et al.: A Hypermedia Tutorial for Cross-Sectional Anatomy: HyperMed . Acta Anatomica, 158, 1997.
C.B. Tresp, R. Molitor: A Description Logic for Vague Knowledge . In European Conference on Artificial Intelligence (ECAI 98), Brighton (England), August 1998.
C.B. Tresp, U. Tüben: Medical Terminology Processing for a Tutoring System . In International Conference on Computational Intelligence and Multimedia Applications (ICCIMA98), Monash Univ. (Australien), Februar 1998.
R. Molitor, C.B. Tresp: Extending Description Logics to Vague Knowledge in Medicine . In P. Szczepaniak, editor, Fuzzy Systems in Medicine, Studies in Fuzziness and Soft Computing. Springer Verlag, 1999. To appear.