1. Inicio
  2. Atrás
Título: Proof theoretical foundations for constructive Description Logic
Autores: Clément, Ian
Fecha: 2008
Publicador: McGill University - MCGILL
Fuente:
Tipo: Electronic Thesis or Dissertation
Tema: Applied Sciences - Computer Science
Descripción: Description logics (DLs) are a family of knowledge representation languages to describe concepts in a given domain. While we can define the semantics of description logics using, for example, a translation into first-order logic, so far the proof-theoretic nature of DL has not been well investigated. In this thesis, we develop a proof theory for a constructive version of Description Logic, specifically Attributive Language with Complement (ALC), in two steps: First, we define a natural deduction system for ALC and develop a sequent calculus formulation, for which we prove cut-admissibility. We build on prior work on constructive description logic by de Paiva [2006] and modal logic by Simpson [1994], which ensures the consistency of the proposed systems for ALC. In addition, we prove soundness and completeness of this system with respect to known Kripke semantics. The study of these properties provides further evidence that it is appropriate to consider description languages as logics. Second, we adapt recent work by Andreoli [1992] on focusing systems for a variety of non-classical logics to the setting of constructive description logics. Exploiting the invertibility of certain inference rules, we design a focusing calculus suitable for backwards search, and prove its correctness via cut-admissibility. This proof-theoretic study lays the foundation for the development of a practical proof search strategy for constructive description logics.
Les logiques descriptives (DLs) sont une famille de langues de representation de connaissance pour décrire les concepts dans un domaine donné. Pendant que nous pouvons définir la sémantique de logiques descriptives en utilisant, par exemple, une traduction dans la logique du premier ordre, pour l'instant la nature théorique de preuve de DL n'a pas été bien enquêtée. Dans cette thèse, nous développons une théorie de preuve pour une version constructive de la logique descriptive, en "Attributive Language with Complement" (ALC ), en deux étapes: Premièrement, nous définissons un système de déduction naturel pour ALC et développons une formulation de calcul de séquent, pour laquelle nous prouvons l'admissibilité de coupure. Nous tirons parti du travail préalable sur la logique descriptive constructive par de Paiva [2006] et la logique modale par Simpson [1994], qui garantit la cohérence des systèmes proposés pour ALC. En plus, nous prouvons la solidité et complétude de ce système par rapport aux sémantiques Kripke connues. L'étude de ces propri étés fournissent plus d'indices que c'est approprié à considérer les langues descriptives comme des logiques propres. Deuxièmement, nous adaptons le travail récent par Andreoli [1992] sur les systèmes concentrés pour une variété de logiques non-classiques au cadre de logiques descriptives constructives. Le fait d'exploiter l'invertibility de certaines règles d'inférences, nous concevons un calcul concentré convenable à recherche reculons et prouvez son exactitude par l'admissibilité de coupure. Cette étude sur une théorie de preuve pose la fondation pour le développement d'une stratégie de recherche de preuves pratiques.
Idioma: en