Advertisement
Published in:
2011 | OriginalPaper | Chapter
Using a Dependently-Typed Language for Expressing Ontologies
Authors : Richard Dapoigny, Patrick Barlatier
Published in: Knowledge Science, Engineering and Management
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Since the last decade the wide spread language for expressing ontologies relies on Description Logics (DLs). However, most of the versions syntactically anchor their modeling primitives on classical logic and require additional theories (i.e., first-order logic, ...) for simultaneously supporting (i) the introduction of constant values (e.g., for individuals) (ii) the limitation of expressiveness for decidability and (iii) the introduction of variables for reasoning with rules. In this paper we show that the introduction of a type theoretical formalism that relies both on a constructive logic and on a typed lambda calculus is able to go beyond these aspects in a single theory. In particular we will show that a number of logical choices (constructive logic, predicative universes for data types, impredicative universe for logic, ...) about the theory will lead to an highly expressive theory which allows for the production of conceptually clean and semantically unambiguous ontologies.