An Overview of Tableau Algorithms for Description Logics

Studia Logica - An International Journal for Symbolic Logic, no. 1 (2001): 5-40

被引用643|浏览13
EI
下载 PDF 全文
引用
微博一下

摘要

Description logics are a family of knowledge representation formalisms that are descended from semantic networks and frames via the system Kl-one. During the last decade, it has been shown that the important reasoning problems (like subsumption and satisfiability) in a great variety of description logics can be decided using tableau-like ...更多

代码

数据

0
简介
  • Description logics (DLs) are a family of knowledge representation languages which can be used to represent the terminological knowledge of an application domain in a structured and formally well-understood way.
  • An ABox is a finite set of assertions of the form C(a) or r(a, b), where C is a concept description, r a role name, and a, b are individual names.
  • Given the input description Cn, the satisfiability algorithm generates a complete and open ABox whose canonical interpretation is a binary tree of depth n, and consists of 2n+1 − 1 individuals.
重点内容
  • Description logics (DLs) are a family of knowledge representation languages which can be used to represent the terminological knowledge of an application domain in a structured and formally well-understood way
  • The name description logics is motivated by the fact that, on the one hand, the important notions of the domain are described by concept descriptions, i.e., expressions that are built from atomic concepts and atomic roles using the concept and role constructors provided by the particular DL
  • Though many of the tableau-based algorithms sketched in this paper are of optimal worst-case complexity, and provide complexity results for subsumption and satisfiability in DLs, theoretical complexity results never were the main focus of this line of DL research
  • For the logics treated in Section 6.2, the exact worst-case complexity (EXPTIME) was known before the (NEXPTIME) tableau algorithms sketched above were designed
  • When the first complexity results showed that all of the DLs used in systems had subsumption problems of a higher complexity, the proposed solution was either to restrict the expressive power or to employ incomplete algorithms
结果
  • For ALCQ, the idea that leads to a PSPACE-algorithm for ALCN with non-unary notation does no longer work: it is not sufficient to introduce just one successor as representative for the role successors required by at-least restrictions.
  • Satisfiability of ALCQ-concept descriptions as well as consistency of ALCQ-ABoxes are PSPACE-complete problems, even if numbers are not represented in unary notation.
  • Nebel (1990b) shows that this complexity can, in general, not be avoided: for the DL FL0, which allows for conjunction and value restriction only, subsumption between concept descriptions can be tested in polynomial time, whereas subsumption w.r.t. acyclic terminologies is coNP-complete.
  • In order to obtain a PSPACE-algorithm for subsumption in ALC w.r.t. acyclic terminologies, one cannot first apply unfolding to the concept descriptions to be tested for subsumption since this may need exponential space.
  • . Internalisation of this axiom introduces a new transitive role u, and asserts in the role hierarchy that u is a super-role of all roles occurring in C and the concept description C0 to be tested for satisfiability.
  • It shows that satisfiability and subsumption of concept descriptions in SH is EXPTIME-hard.5 The tableau algorithm for SH presented in (Horrocks, 1998b) handles role hierarchies by an appropriate definition of r-successors: an individual y is called an r-successor of an individual x in an ABox A iff s(x, y) ∈ A for some sub-role s of r.
  • This violates the value restriction for x1, which shows that the interpretation obtained this way is not a model of the complete and open ABox. This problem can be overcome by using equality blocking, i.e., an individual y is blocked by an individual x iff {D | D(x) ∈ A} = {D | D (y) ∈ A}.
结论
  • If the role hierarchy contains the axiom s r for a transitive role r ∈ NR+, the following concept is obviously satisfiable, but each of its models has an infinite s-path: ¬A ∃s.A ∀r.(∃s.A ( 1s−)).
  • This problem can be overcome by applying the pre-completion technique, which reduces ABox consistency to satisfiability of concept descriptions.
  • It turned out that implementations of these algorithms were amenable to optimisation techniques and behaved quite well in practice (Baader et al, 1994; Bresciani et al, 1995)
总结
  • Description logics (DLs) are a family of knowledge representation languages which can be used to represent the terminological knowledge of an application domain in a structured and formally well-understood way.
  • An ABox is a finite set of assertions of the form C(a) or r(a, b), where C is a concept description, r a role name, and a, b are individual names.
  • Given the input description Cn, the satisfiability algorithm generates a complete and open ABox whose canonical interpretation is a binary tree of depth n, and consists of 2n+1 − 1 individuals.
  • For ALCQ, the idea that leads to a PSPACE-algorithm for ALCN with non-unary notation does no longer work: it is not sufficient to introduce just one successor as representative for the role successors required by at-least restrictions.
  • Satisfiability of ALCQ-concept descriptions as well as consistency of ALCQ-ABoxes are PSPACE-complete problems, even if numbers are not represented in unary notation.
  • Nebel (1990b) shows that this complexity can, in general, not be avoided: for the DL FL0, which allows for conjunction and value restriction only, subsumption between concept descriptions can be tested in polynomial time, whereas subsumption w.r.t. acyclic terminologies is coNP-complete.
  • In order to obtain a PSPACE-algorithm for subsumption in ALC w.r.t. acyclic terminologies, one cannot first apply unfolding to the concept descriptions to be tested for subsumption since this may need exponential space.
  • . Internalisation of this axiom introduces a new transitive role u, and asserts in the role hierarchy that u is a super-role of all roles occurring in C and the concept description C0 to be tested for satisfiability.
  • It shows that satisfiability and subsumption of concept descriptions in SH is EXPTIME-hard.5 The tableau algorithm for SH presented in (Horrocks, 1998b) handles role hierarchies by an appropriate definition of r-successors: an individual y is called an r-successor of an individual x in an ABox A iff s(x, y) ∈ A for some sub-role s of r.
  • This violates the value restriction for x1, which shows that the interpretation obtained this way is not a model of the complete and open ABox. This problem can be overcome by using equality blocking, i.e., an individual y is blocked by an individual x iff {D | D(x) ∈ A} = {D | D (y) ∈ A}.
  • If the role hierarchy contains the axiom s r for a transitive role r ∈ NR+, the following concept is obviously satisfiable, but each of its models has an infinite s-path: ¬A ∃s.A ∀r.(∃s.A ( 1s−)).
  • This problem can be overcome by applying the pre-completion technique, which reduces ABox consistency to satisfiability of concept descriptions.
  • It turned out that implementations of these algorithms were amenable to optimisation techniques and behaved quite well in practice (Baader et al, 1994; Bresciani et al, 1995)
表格
  • Table1: Syntax and semantics of concept descriptions. From the modal logic point of view, roles are simply names for accessibility relations, and existential (value) restrictions correspond to diamonds (boxes) indexed by the respective accessibility relation. Thus, any ALC description can be translated into a multi-modal K formula and vice versa. For example, the description P ∃r.P ∀r.¬P corresponds to the formula p ∧ r p ∧ [r]¬p, where p is an atomic proposition corresponding to the concept name P . As pointed out by <a class="ref-link" id="cSchild_1991_a" href="#rSchild_1991_a">Schild (1991</a>), there is an obvious correspondence between the semantics of ALC and the Kripke semantics for
  • Table2: Syntax and semantics of role constructors and restrictions
Download tables as Excel
引用论文
  • Baader, F.: 1991, ‘Augmenting Concept Languages by Transitive Closure of Roles: An Alternative to Terminological Cycles’. In: Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI-91). A long version appeared as DFKI-Research-Report RR-90-13, Kaiserslautern, Germany.
    Google ScholarLocate open access versionFindings
  • Baader, F., M. Buchheit, and B. Hollunder: 1996, ‘Cardinality Restrictions on Concepts’. Artificial Intelligence Journal 88(1–2), 195–213.
    Google ScholarLocate open access versionFindings
  • Baader, F., H.-J. Burckert, B. Nebel, W. Nutt, and G. Smolka: 1993, ‘On the Expressivity of Feature Logics with Negation, Functional Uncertainty, and Sort Equations’. Journal of Logic, Language and Information 2, 1–18.
    Google ScholarLocate open access versionFindings
  • Baader, F., E. Franconi, B. Hollunder, B. Nebel, and H. Profitlich: 1994, ‘An Empirical Analysis of Optimization Techniques for Terminological Representation Systems or: Making KRIS get a move on’. Applied Artificial Intelligence. Special Issue on Knowledge Base Management 4, 109–132.
    Google ScholarLocate open access versionFindings
  • Baader, F. and P. Hanschke: 1991, ‘A Schema for Integrating Concrete Domains into Concept Languages’. Technical Report RR-91-10, Deutsches Forschungszentrum fur Kunstliche Intelligenz (DFKI), Kaiserslautern, Germany. An abridged version appeared in Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI-91).
    Google ScholarFindings
  • Baader, F. and B. Hollunder: 1991, ‘A Terminological Knowledge Representation System with Complete Inference Algorithm’. In: Proc. of PDK’91, Vol. 567 of Lecture Notes In Artificial Intelligence. pp. 67–86, Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • Baader, F. and U. Sattler: 1999, ‘Expressive Number Restrictions in Description Logics’. Journal of Logic and Computation 9(3), 319–350.
    Google ScholarLocate open access versionFindings
  • Baader, F. and U. Sattler: 2000, ‘Tableau Algorithms for Description Logics’. In: R. Dyckhoff (ed.): Proc. of the Int. Conf. on Automated Reasoning with Tableaux and Related Methods (Tableaux 2000), Vol. 1847 of Lecture Notes in Artificial Intelligence. pp. 1–18, Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • Ben-Ari, M., J. Y. Halpern, and A. Pnueli: 1982, ‘Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness’. Journal of Computer and System Science 25, 402–417.
    Google ScholarLocate open access versionFindings
  • Borgida, A. and P. F. Patel-Schneider: 1994, ‘A Semantics and Complete Algorithm for Subsumption in the CLASSIC Description Logic’. Journal of Artificial Intelligence Research 1, 277–308.
    Google ScholarLocate open access versionFindings
  • Brachman, R. J.: 1992, ‘“Reducing” CLASSIC to Practice: Knowledge Representation Meets Reality’. In: Proc. of the 3rd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-92). pp. 247–258, Morgan Kaufmann.
    Google ScholarLocate open access versionFindings
  • Brachman, R. J. and H. J. Levesque: 1984, ‘The Tractability of Subsumption in FrameBased Description Languages’. In: Proc. of the 4th Nat. Conf. on Artificial Intelligence (AAAI-84), pp. 34–37, AAAI Press.
    Google ScholarLocate open access versionFindings
  • Brachman, R. J. and H. J. Levesque (eds.): 1985, Readings in Knowledge Representation. Morgan Kaufmann.
    Google ScholarLocate open access versionFindings
  • Brachman, R. J. and J. G. Schmolze: 1985, ‘An Overview of the KL-ONE Knowledge Representation System’. Cognitive Science 9(2), 171–216.
    Google ScholarLocate open access versionFindings
  • Bresciani, P., E. Franconi, and S. Tessaris: 1995, ‘Implementing and Testing Expressive Description Logics: Preliminary Report’. In: A. Borgida, M. Lenzerini, D. Nardi, and B. Nebel (eds.): Working Notes of the 1995 Description Logics Workshop. pp. 131–139.
    Google ScholarLocate open access versionFindings
  • Buchheit, M., F. M. Donini, and A. Schaerf: 1993, ‘Decidable Reasoning in Terminological Knowledge Representation Systems’. Journal of Artificial Intelligence Research 1, 109– 138.
    Google ScholarLocate open access versionFindings
  • Calvanese, D., G. De Giacomo, and M. Lenzerini: 1998a, ‘On the Decidability of Query Containment under Constraints’. In: Proc. of the Seventeenth ACM SIGACT SIGMOD Sym. on Principles of Database Systems (PODS-98). pp. 149–158.
    Google ScholarLocate open access versionFindings
  • Calvanese, D., G. De Giacomo, M. Lenzerini, D. Nardi, and R. Rosati: 1998b, ‘Description Logic Framework for Information Integration’. In: Proc. of the 6th Int. Conf. on the
    Google ScholarLocate open access versionFindings
  • Calvanese, D., G. De Giacomo, and R. Rosati: 1999a, ‘Data Integration and Reconciliation in Data Warehousing: Conceptual Modeling and Reasoning Support’. Network and Information Systems 4(2).
    Google ScholarLocate open access versionFindings
  • Calvanese, D., G. D. Giacomo, M. Lenzerini, and D. Nardi: 2001, ‘Reasoning in Expressive Description Logics’. In: A. Robinson and A. Voronkov (eds.): Handbook of Automated Reasoning. Amsterdam, NL: Elsevier Science Publishers.
    Google ScholarLocate open access versionFindings
  • Calvanese, D., M. Lenzerini, and D. Nardi: 1998c, ‘Description Logics for Conceptual Data Modeling’. In: J. Chomicki and G. Saake (eds.): Logics for Databases and Information Systems. Kluwer Academic Publisher, pp. 229–264.
    Google ScholarLocate open access versionFindings
  • Calvanese, D., M. Lenzerini, and D. Nardi: 1999b, ‘Unifying Class-Based Representation Formalisms’. Journal of Artificial Intelligence Research 11, 199–240.
    Google ScholarLocate open access versionFindings
  • De Giacomo, G.: 1995, ‘Decidability of Class-Based Knowledge Representation Formalisms’. Ph.D. thesis, Dipartimento di Informatica e Sistemistica, Universita di Roma “La Sapienza”.
    Google ScholarFindings
  • De Giacomo, G., F. Donini, and F. Massacci: 1996, ‘EXPTIME tableaux for ALC’. In: Proc. of the 1996 Description Logic Workshop (DL’96).
    Google ScholarFindings
  • De Giacomo, G. and M. Lenzerini: 1994, ‘Boosting the Correspondence between Description Logics and Propositional Dynamic Logics’. In: Proc. of the 12th Nat. Conf. on Artificial Intelligence (AAAI-94). pp. 205–212, AAAI Press/The MIT Press.
    Google ScholarLocate open access versionFindings
  • De Giacomo, G. and M. Lenzerini: 1996, ‘TBox and ABox Reasoning in Expressive Description Logics’. In: L. C. Aiello, J. Doyle, and S. C. Shapiro (eds.): Proc. of the 5th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-96). pp. 316–327, Morgan Kaufmann.
    Google ScholarLocate open access versionFindings
  • De Giacomo, G. and F. Massacci: 1996, ‘Tableaux and algorithms for propositional dynamic logic with converse’. In: Proc. of the 13th Conf. on Automated Deduction (CADE-96), Vol. 1104 of Lecture Notes In Artificial Intelligence. pp. 613–628, SpringerVerlag. A long versioned will appear in Information and Computation.
    Google ScholarLocate open access versionFindings
  • Donini, F. M., B. Hollunder, M. Lenzerini, A. M. Spaccamela, D. Nardi, and W. Nutt: 1992, ‘The Complexity of Existential Quantification in Concept Languages’. Artificial Intelligence Journal 2–3, 309–327.
    Google ScholarLocate open access versionFindings
  • Donini, F. M., M. Lenzerini, D. Nardi, and W. Nutt: 1991a, ‘The Complexity of Concept Languages’. In: J. Allen, R. Fikes, and E. Sandewall (eds.): Proc. of the 2nd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-91). pp. 151–162, Morgan Kaufmann.
    Google ScholarLocate open access versionFindings
  • Donini, F. M., M. Lenzerini, D. Nardi, and W. Nutt: 1991b, ‘Tractable Concept Languages’. In: Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI-91). pp. 458–463.
    Google ScholarLocate open access versionFindings
  • Donini, F. M., M. Lenzerini, D. Nardi, and A. Schaerf: 1994, ‘Deduction in Concept Languages: From Subsumption to Instance Checking’. Journal of Logic and Computation 4(4), 423–452.
    Google ScholarLocate open access versionFindings
  • Donini, F. M., M. Lenzerini, D. Nardi, and A. Schaerf: 1996, ‘Reasoning in Description Logics’. In: G. Brewka (ed.): Principles of Knowledge Representation, Studies in Logic, Language and Information. CSLI Publications, pp. 193–238.
    Google ScholarLocate open access versionFindings
  • Donini, F. M. and F. Massacci: 1999, ‘EXPTIME Tableaux for ALC’. Technical Report 32/99, Dipartimento di Ingegenria dell’Informazione, Universita degli studi di Siena, Italy. To appear in Artificial Intelligence.
    Google ScholarFindings
  • Franconi, E. and G. Ng: 2000, ‘The i•com Tool for Intelligent Conceptual Modelling’. In: Working Notes of the ECAI2000 Workshop on Knowledge Representation Meets Databases (KRDB2000), CEUR Electronic Workshop Proceedings.
    Google ScholarLocate open access versionFindings
  • Franconi, E. and U. Sattler: 1999, ‘A Data Warehouse Conceptual Data Model for Multidimensional Aggregation: a preliminary report’. Italian Association for Artificial Intelligence AI*IA Notizie 1, 9–21.
    Google ScholarLocate open access versionFindings
  • Haarslev, V. and R. Moller: 1999, ‘RACE System Description’. In: Proc. of the 1999 Description Logic Workshop (DL’99). pp. 130–132, CEUR Electronic Workshop Proceedings.
    Google ScholarLocate open access versionFindings
  • Haarslev, V. and R. Moller: 2000a, ‘Consistency Testing: The RACE Experience’. In: R. Dyckhoff (ed.): Proc. of the Int. Conf. on Automated Reasoning with Tableaux and Related Methods (Tableaux 2000), Vol. 1847 of Lecture Notes in Artificial Intelligence. pp. 57–61, Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • Haarslev, V. and R. Moller: 2000b, ‘Expressive ABox Reasoning with Number Restrictions, Role Hierarchies, and Transitively Closed Roles’. In: Proc. of the 7th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-00). Morgan Kaufmann.
    Google ScholarLocate open access versionFindings
  • Halpern, J. Y. and Y. Moses: 1992, ‘A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief’. Artificial Intelligence Journal 54, 319–379.
    Google ScholarLocate open access versionFindings
  • Hanschke, P.: 1992, ‘Specifying Role Interaction in Concept Languages’. In: Proc. of the 3rd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-92). pp. 318–329, Morgan Kaufmann.
    Google ScholarLocate open access versionFindings
  • Harel, D.: 1984, ‘Dynamic Logic’. In: Handbook of Philosophical Logic, Vol. 2.
    Google ScholarLocate open access versionFindings
  • Hollunder, B.: 1990, ‘Hybrid Inferences in KL-ONE-based Knowledge Representation Systems’. In: Proc. of GWAI’90, Vol. 251 of Informatik-Fachberichte. pp. 38–47, SpringerVerlag.
    Google ScholarLocate open access versionFindings
  • Hollunder, B.: 1996, ‘Consistency Checking Reduced to Satisfiability of Concepts in Terminological Systems’. Annals of Mathematics and Artificial Intelligence 18(2–4), 133–157.
    Google ScholarLocate open access versionFindings
  • Hollunder, B. and F. Baader: 1991, ‘Qualifying Number Restrictions in Concept Languages’. In: Proc. of the 2nd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-91). pp. 335–346, Morgan Kaufmann.
    Google ScholarLocate open access versionFindings
  • Hollunder, B. and W. Nutt: 1990, ‘Subsumption Algorithms for Concept Languages’. Technical Report RR-90-04, Deutsches Forschungszentrum fur Kunstliche Intelligenz (DFKI), Kaiserslautern, Germany.
    Google ScholarFindings
  • Hollunder, B., W. Nutt, and M. Schmidt-Schauß: 1990, ‘Subsumption Algorithms for Concept Description Languages’. In: Proc. of the 9th European Conf. on Artificial Intelligence (ECAI-90). pp. 348–353, Pitman.
    Google ScholarLocate open access versionFindings
  • Horrocks, I.: 1998a, ‘The FaCT System’. In: H. de Swart (ed.): Proc. of the Int. Conf. on Automated Reasoning with Tableaux and Related Methods (Tableaux-98), Vol. 1397 of Lecture Notes in Artificial Intelligence. pp. 307–312, Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • Horrocks, I.: 1998b, ‘Using an Expressive Description Logic: FaCT or Fiction?’. In: Proc. of the 6th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-98). pp. 636–647, Morgan Kaufmann.
    Google ScholarLocate open access versionFindings
  • Horrocks, I.: 2000, ‘Benchmark Analysis for FaCT’. In: R. Dyckhoff (ed.): Proc. of the Int. Conf. on Automated Reasoning with Tableaux and Related Methods (Tableaux 2000), Vol. 1847 of Lecture Notes in Artificial Intelligence. pp. 62–66, Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • Horrocks, I. and P. F. Patel-Schneider: 1999, ‘Optimizing Description Logic Subsumption’. Journal of Logic and Computation 9(3), 267–293.
    Google ScholarLocate open access versionFindings
  • Horrocks, I. and U. Sattler: 1999, ‘A Description Logic with Transitive and Inverse Roles and Role Hierarchies’. Journal of Logic and Computation 9(3), 385–410.
    Google ScholarLocate open access versionFindings
  • Horrocks, I., U. Sattler, and S. Tobies: 1999, ‘Practical Reasoning for Expressive Description Logics’. In: Proc. of the 6th Int. Conf. on Logic for Programming and Automated Reasoning (LPAR’99), Vol. 1705 of Lecture Notes In Artificial Intelligence. SpringerVerlag.
    Google ScholarLocate open access versionFindings
  • Horrocks, I., U. Sattler, and S. Tobies: 2000a, ‘Practical Reasoning for Very Expressive Description Logics’. Logic Journal of the IGPL 8(3), 239–264.
    Google ScholarLocate open access versionFindings
  • Horrocks, I., U. Sattler, and S. Tobies: 2000b, ‘Reasoning with Individuals for the Description Logic SHIQ’. In: D. MacAllester (ed.): Proc. of the 13th Conf. on Automated Deduction (CADE-17). Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • Lutz, C.: 1999, ‘Complexity of Terminological Reasoning Revisited’. In: Proc. of the 6th Int. Conf. on Logic for Programming and Automated Reasoning (LPAR’99), Vol. 1705 of Lecture Notes In Artificial Intelligence. Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • Lutz, C. and U. Sattler: 2000, ‘The Complexity of Reasoning with Boolean Modal Logic’. In: Advances in Modal Logic 2000 (AiML 2000). Leipzig, Germany.
    Google ScholarLocate open access versionFindings
  • MacGregor, R.: 1991, ‘The Evolving Technology of Classification-Based Knowledge Representation Systems’. In: J. F. Sowa (ed.): Principles of Semantic Networks. Morgan Kaufmann, pp. 385–400.
    Google ScholarLocate open access versionFindings
  • Mays, E., R. Dionne, and R. Weida: 1991, ‘K-REP System Overview’. SIGART Bulletin 2(3).
    Google ScholarLocate open access versionFindings
  • Minsky, M.: 1981, ‘A Framework for Representing Knowledge’. In: J. Haugeland (ed.): Mind Design. The MIT Press. Republished in (Brachman and Levesque, 1985).
    Google ScholarLocate open access versionFindings
  • Nebel, B.: 1990a, Reasoning and Revision in Hybrid Representation Systems, Vol. 422 of Lecture Notes In Artificial Intelligence. Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • Nebel, B.: 1990b, ‘Terminological Reasoning is Inherently Intractable’. Artificial Intelligence Journal 43, 235–249.
    Google ScholarLocate open access versionFindings
  • Nebel, B.: 1991, ‘Terminological Cycles: Semantics and Computational Properties’. In: J. F. Sowa (ed.): Principles of Semantic Networks. Morgan Kaufmann, pp. 331–361.
    Google ScholarLocate open access versionFindings
  • Patel-Schneider, P.: 2000, ‘TANCS-2000 Results for DLP’. In: R. Dyckhoff (ed.): Proc. of the Int. Conf. on Automated Reasoning with Tableaux and Related Methods (Tableaux 2000), Vol. 1847 of Lecture Notes in Artificial Intelligence. pp. 72–76, Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • Patel-Schneider, P. F.: 1999, ‘DLP’. In: Proc. of the 1999 Description Logic Workshop (DL’99). pp. 9–13, CEUR Electronic Workshop Proceedings.
    Google ScholarLocate open access versionFindings
  • Patel-Schneider, P. F. and I. Horrocks: 1999, ‘DLP and FaCT’. In: Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-99), Vol. 1397 of Lecture Notes In Artificial Intelligence. pp. 19–23, Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • Patel-Schneider, P. F., D. L. McGuiness, R. J. Brachman, L. A. Resnick, and A. Borgida: 1991, ‘The CLASSIC Knowledge Representation System: Guiding Principles and Implementation Rational’. SIGART Bulletin 2(3), 108–113.
    Google ScholarLocate open access versionFindings
  • Peltason, C.: 1991, ‘The BACK System – an Overview’. SIGART Bulletin 2(3), 114–119.
    Google ScholarLocate open access versionFindings
  • Pratt, V. R.: 1979, ‘Models of Program Logic’. In: Proc. of the 20th Annual Sym. on the Foundations of Computer Science (FOCS-79). pp. 115–122.
    Google ScholarLocate open access versionFindings
  • Quillian, M. R.: 1967, ‘Word Concepts: A Theory and Simulation of Some Basic Capabilities’. Behavioral Science 12, 410–430. Republished in (Brachman and Levesque, 1985).
    Google ScholarLocate open access versionFindings
  • Sattler, U.: 1996, ‘A Concept Language Extended with Different Kinds of Transitive Roles’. In: G. Gorz and S. Holldobler (eds.): Proc. of the 20th German Annual Conf. on Artificial Intelligence (KI’96), Vol. 1137 of Lecture Notes In Artificial Intelligence. Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • Savitch, W. J.: 1970, ‘Relationship between Nondeterministic and Deterministic Tape Complexities’. Journal of Computer and System Science 4, 177–192.
    Google ScholarLocate open access versionFindings
  • Schaerf, A.: 1993, ‘On the Complexity of the Instance Checking Problem in Concept Languages with Existential Quantification’. Journal of Intelligent Information Systems 2, 265–278.
    Google ScholarLocate open access versionFindings
  • Schild, K.: 1991, ‘A Correspondence Theory for Terminological Logics: Preliminary Report’. In: Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI-91). pp. 466–471.
    Google ScholarLocate open access versionFindings
  • Schild, K.: 1994, ‘Terminological Cycles and the Propositional μ-Calculus’. In: J. Doyle, E. Sandewall, and P. Torasso (eds.): Proc. of the 4th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-94). pp. 509–520, Morgan Kaufmann.
    Google ScholarLocate open access versionFindings
  • Schmidt-Schauß, M.: 1989, ‘Subsumption in KL-ONE is Undecidable’. In: R. J. Brachman, H. J. Levesque, and R. Reiter (eds.): Proc. of the 1st Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-89). pp. 421–431, Morgan Kaufmann.
    Google ScholarLocate open access versionFindings
  • Schmidt-Schauß, M. and G. Smolka: 1991, ‘Attributive Concept Descriptions with Complements’. Artificial Intelligence Journal 48(1), 1–26.
    Google ScholarLocate open access versionFindings
  • Spaan, E.: 1993, ‘The Complexity of Propositional Tense Logics’. In: M. de Rijke (ed.): Diamonds and Defaults. Kluwer Academic Publishers, pp. 287–307.
    Google ScholarLocate open access versionFindings
  • Stirling, C.: 1992, ‘Modal and Temporal Logic’. In: S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum (eds.): Handbook of Logic in Computer Science. Clarendon Press, pp. 477–563.
    Google ScholarLocate open access versionFindings
  • Tobies, S.: 1999, ‘A PSPACE Algorithm for Graded Modal Logic’. In: Proc. of the 13th Conf. on Automated Deduction (CADE-16), Vol. 1632 of Lecture Notes in Computer Science. Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • Van der Hoek, W. and M. De Rijke: 1995, ‘Counting Objects’. Journal of Logic and Computation 5(3), 325–345.
    Google ScholarLocate open access versionFindings
  • Vardi, M. Y. and P. Wolper: 1986, ‘Automata-theoretic Techniques for Modal Logics of Programs’. Journal of Computer and System Science 32, 183–221. A preliminary version appeared in Proc. of the 16th ACM SIGACT Symp. on Theory of Computing (STOC’84).
    Google ScholarLocate open access versionFindings
作者
Franz Baader
Franz Baader
您的评分 :
0

 

标签
评论
小科