Abstract
In the domain of ontology design as well as in Conceptual Modeling, representing universals is a challenging problem. Most approaches which have addressed this problem rely either on Description Logics (DLs) or on First Order Logic (FOL), but many difficulties remain especially about expressiveness. In mathematical logic and program checking, type theories have proved to be appealing but so far, they have not been applied in the formalization of ontologies. To bridge this gap, we present here the main capabilities of a theory for representing ontological structures in a dependently-typed framework which relies both on a constructive logic and on a functional type system. The usability of the theory is demonstrated with the Coq language which defines in a precise way what ontological primitives such as classes, relations, properties and meta-properties, are in terms of type classes.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alia, I., Abdelmoty, A.I., Smart, P.D., Jones, C.B., Fu, G., Finch, D.: A critical evaluation of ontology languages for geographic information retrieval on the Internet. Journal of Visual Languages & Computing 16(4), 331–358 (2005)
Barlatier, P., Dapoigny, R.: A Type-Theoretical Approach for Ontologies: the Case of Roles. Applied Ontology 73, 311–356 (in press, 2012)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS series. Springer (2004)
Bodenreider, O., Smith, B., Kumar, A., Burgun, A.: Investigating subsumption in SNOMED CT: An exploration into large description logic-based biomedical terminologies. Artificial Intelligence in Medicine 39, 183–195 (2007)
Booch, G.: Object-Oriented Design with Applications. Benjamin Cummings, Redwood City (1991)
Bourbaki, N.: Univers, Séminaire de Géométrie Algébrique du Bois Marie Théorie des topos et cohomologie étale des schémas (SGA 4), 1. Lecture notes in mathematics, vol. 269, pp. 185–217. Springer (1972)
Chein, M., Mugnier, M.L., Simonet, G.: Nested graphs: a graph-based knowledge representation model with FOL semantics. In: Procs. of KR 1998, pp. 524–534. Morgan Kaufmann (1998)
Cirstea, H., Coquery, E., Drabent, W., Fages, F., Kirchner, C., Maluszynski, J., Wack, B.: Types for Web Rule Languages: a preliminary study. Technical report A04-R-560, PROTHEO - INRIA Lorraine - LORIA (2004)
Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76(2-3), 95–120 (1988)
Coq Development Team, The Coq Reference Manual, Version 8.3., INRIA, France (2010)
Dapoigny, R., Barlatier, P.: Towards Ontological Correctness of Part-whole Relations with Dependent Types. In: Procs. of the Sixth Int. Conference (FOIS 2010), pp. 45–58 (2010a)
Dapoigny, R., Barlatier, P.: Modeling Contexts with Dependent Types. Fundamenta Informaticae 104(4), 293–327 (2010b)
Eiter, T., Lukasiewicz, T., Schindlauer, R., Tompits, H.: Combining answer set programming with description logics for the semantic web. In: Proc. of Ninth Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR 2004), pp. 141–151. AAAI Press (2004)
Angelov, K., Enache, R.: Typeful Ontologies with Direct Multilingual Verbalization. In: Rosner, M., Fuchs, N.E. (eds.) CNL 2010. LNCS, vol. 7175, pp. 1–20. Springer, Heidelberg (2012)
Gangemi, A., Guarino, N., Masolo, C., Oltramari, A., Schneider, L.: Sweetening Ontologies with DOLCE. In: Gómez-Pérez, A., Benjamins, V.R. (eds.) EKAW 2002. LNCS (LNAI), vol. 2473, pp. 166–181. Springer, Heidelberg (2002)
Guarino, N.: The Ontological Level. In: Casati, R., Smith, B., White, G. (eds.) Philosophy and the Cognitive Science, pp. 443–456. Holder-Pivhler-Tempsky (1994)
Guarino, N., Welty, C.: An Overview of OntoClean. In: Handbook on Ontologies, pp. 151–172 (2004)
Guarino, N.: The Ontological Level: Revisiting 30 Years of Knowledge Representation. In: Borgida, A.T., Chaudhri, V.K., Giorgini, P., Yu, E.S. (eds.) Conceptual Modeling: Foundations and Applications. LNCS, vol. 5600, pp. 52–67. Springer, Heidelberg (2009)
Guizzardi, G., Herre, H., Wagner, G.: On the General Ontological Foundations of Conceptual Modeling. In: Spaccapietra, S., March, S.T., Kambayashi, Y. (eds.) ER 2002. LNCS, vol. 2503, pp. 65–78. Springer, Heidelberg (2002)
Guizzardi, G.: Ontological Foundations for Structural Conceptual Models. University of Twente (Centre for Telematics and Information Technology) (2005)
Guizzardi, G., Masolo, C., Borgo, S.: In Defense of a Trope-Based Ontology for Conceptual Modeling: An Example with the Foundations of Attributes, Weak Entities and Datatypes. In: Embley, D.W., Olivé, A., Ram, S. (eds.) ER 2006. LNCS, vol. 4215, pp. 112–125. Springer, Heidelberg (2006)
Howard, W.A.: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. The formulae-as-types notion of construction, pp. 479–490. Academic Press (1980)
Kabbaj, A., Janta-Polczynski, M.: From PROLOG+ + to PROLOG+CG: A CG Object-Oriented Logic Programming Language, B. In: Ganter, B., Mineau, G.W. (eds.) ICCS 2000. LNCS (LNAI), vol. 1867, pp. 540–554. Springer, Heidelberg (2000)
Kaneiwa, K., Mizoguchi, R.: Ontological Knowledge Base Reasoning with Sort-Hierarchy and Rigidity. In: Procs. of KR 2004, pp. 278–288. AAAI Press (2004)
Keet, C.M., Artale, A.: Representing and reasoning over a taxonomy of part-whole relations. Applied Ontology 3(1-2), 91–110 (2008)
Kifer, M., Lausen, G., Wu, J.: Logical foundations of object-oriented and frame-based languages. Journal of the ACM 42, 741–843 (1995)
Krötzsch, M., et al.: How to reason with OWL in a logic programming system. In: Procs. of RuleML 2006 (2006)
Luo, Z.: Coercive subtyping. Journal of Logic and Computation 9(1), 105–130 (1999)
Masolo, C., Borgo, S., Gangemi, A., Guarino, N., Oltramari, A.: Ontology Library (D18). Laboratory for Applied Ontology-ISTC-CNR (2003)
McKinna, J.: Why dependent types matter. In: Procs. of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol. 41(1), p. 1 (2006)
Mugnier, M.L., Leclère, M.: On querying simple conceptual graphs with negation. Data & Knowledge engineering 60(3), 468–493 (2007)
Mylopoulos, J., Borgida, A., Jarke, M., Koubarakis, M.: Telos: Representing Knowledge About Information Systems. ACM Trans. on Information Systems 8(4), 325–362 (1990)
Napoli, A.: Subsumption and classification-based reasoning in object-based representations. In: Procs. of the 10th European Conference on Artificial Intelligence (ECAI 1992), pp. 425–429. John Wiley & Sons Ltd. (1992)
Noonan, H.: Identity. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (2011), http://plato.stanford.edu/archives/win2011/entries/identity/
Pires, L.F., van Sinderen, M., Munthe-Kaas, E., Prokaev, S.M.H., Plas, D.J.: Techniques for describing and manipulating context information, Freeband/A MUSE D3.5v2.0, Lucent Technologies (2005)
Paulin-Mohring, C.: Inductive Definitions in the System Coq - Rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328–345. Springer, Heidelberg (1993)
Rosati, R.: DL+log: Tight integration of description logics and disjunctive datalog. In: Proc. of Tenth Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2006), pp. 68–78. AAAI Press (2006)
Saibi, A.: Typing algorithm in type theory with inheritance. In: Procs. of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1997), pp. 292–301. ACM Press (1997)
Setzer, A.: Object-Oriented Programming in Dependent Type Theory. In: Trends in Functional Programming, Intellect, vol. 7, pp. 91–108 (2007)
Smith, B., Rosse, C.: The Role of Foundational Relations in the Alignment of Biomedical Ontologies. In: Fieschi, M., et al. (eds.) MEDINFO 2004. IOS Press, Amsterdam (2004)
Sozeau, M., Oury, N.: First-Class Type Classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008)
Sowa, J.F.: Using a lexicon of canonical graphs in a semantic interpreter. Relational models of the lexicon, pp. 113–137. Cambridge University Press (1988)
Sowa, J.F.: Knowledge Representation: Logical, Philosophical, and Computational Foundations. Brooks Cole Publishing Co., Pacific Grove (2000)
Sowa, J.F.: Conceptual Graphs. In: van Harmelen, F., Lifschitz, V., Porter, B. (eds.) Handbook of Knowledge Representation, ch. 5, pp. 213–237. Elsevier (2008)
Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Mathematical Structures in Computer Science 21(4), 795–825 (2011)
Werner, B.: On the strength of proof-irrelevant type theories. Logical Methods in Computer Science 4(3) (2008)
Woods, W.A.: Understanding Subsumption and Taxonomy: a Framework for progress. In: Sowa, J. (ed.) Principles of Semantic Networks, pp. 45–94. Morgan Kaufmann (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dapoigny, R., Barlatier, P. (2013). Modeling Ontological Structures with Type Classes in Coq. In: Pfeiffer, H.D., Ignatov, D.I., Poelmans, J., Gadiraju, N. (eds) Conceptual Structures for STEM Research and Education. ICCS 2013. Lecture Notes in Computer Science(), vol 7735. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35786-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-35786-2_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35785-5
Online ISBN: 978-3-642-35786-2
eBook Packages: Computer ScienceComputer Science (R0)