Modeling Ontological Structures with Type Classes in Coq
Identifieur interne : 001536 ( Main/Exploration ); précédent : 001535; suivant : 001537Modeling Ontological Structures with Type Classes in Coq
Auteurs : Richard Dapoigny [France] ; Patrick Barlatier [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
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.
Url:
DOI: 10.1007/978-3-642-35786-2_11
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002A36
- to stream Istex, to step Curation: 002999
- to stream Istex, to step Checkpoint: 000162
- to stream Main, to step Merge: 001548
- to stream Main, to step Curation: 001536
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Modeling Ontological Structures with Type Classes in Coq</title><author><name sortKey="Dapoigny, Richard" sort="Dapoigny, Richard" uniqKey="Dapoigny R" first="Richard" last="Dapoigny">Richard Dapoigny</name></author><author><name sortKey="Barlatier, Patrick" sort="Barlatier, Patrick" uniqKey="Barlatier P" first="Patrick" last="Barlatier">Patrick Barlatier</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:B2A3CEE6282E5E7BDE209FB329E6BDE8E2F07954</idno><date when="2013" year="2013">2013</date><idno type="doi">10.1007/978-3-642-35786-2_11</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-NFWL333N-8/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002A36</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002A36</idno><idno type="wicri:Area/Istex/Curation">002999</idno><idno type="wicri:Area/Istex/Checkpoint">000162</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000162</idno><idno type="wicri:doubleKey">0302-9743:2013:Dapoigny R:modeling:ontological:structures</idno><idno type="wicri:Area/Main/Merge">001548</idno><idno type="wicri:Area/Main/Curation">001536</idno><idno type="wicri:Area/Main/Exploration">001536</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Modeling Ontological Structures with Type Classes in Coq</title><author><name sortKey="Dapoigny, Richard" sort="Dapoigny, Richard" uniqKey="Dapoigny R" first="Richard" last="Dapoigny">Richard Dapoigny</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LISTIC/Polytech’Annecy-Chambéry, University of Savoie, P.O. Box 80439, 74944, Annecy-le-vieux cedex</wicri:regionArea><placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region><region type="old region" nuts="2">Rhône-Alpes</region><settlement type="city">Annecy-le-vieux</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Barlatier, Patrick" sort="Barlatier, Patrick" uniqKey="Barlatier P" first="Patrick" last="Barlatier">Patrick Barlatier</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LISTIC/Polytech’Annecy-Chambéry, University of Savoie, P.O. Box 80439, 74944, Annecy-le-vieux cedex</wicri:regionArea><placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region><region type="old region" nuts="2">Rhône-Alpes</region><settlement type="city">Annecy-le-vieux</settlement></placeName></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">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.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Auvergne-Rhône-Alpes</li><li>Rhône-Alpes</li></region><settlement><li>Annecy-le-vieux</li></settlement></list><tree><country name="France"><region name="Auvergne-Rhône-Alpes"><name sortKey="Dapoigny, Richard" sort="Dapoigny, Richard" uniqKey="Dapoigny R" first="Richard" last="Dapoigny">Richard Dapoigny</name></region><name sortKey="Barlatier, Patrick" sort="Barlatier, Patrick" uniqKey="Barlatier P" first="Patrick" last="Barlatier">Patrick Barlatier</name><name sortKey="Dapoigny, Richard" sort="Dapoigny, Richard" uniqKey="Dapoigny R" first="Richard" last="Dapoigny">Richard Dapoigny</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001536 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001536 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:B2A3CEE6282E5E7BDE209FB329E6BDE8E2F07954
|texte= Modeling Ontological Structures with Type Classes in Coq
}}
| This area was generated with Dilib version V0.6.33. |  |