Abstract
The use of formal languages in the specification of upper ontologies helps establishing precise and unambiguous definitions for its concepts and relations. In this context, the use of formal languages with support of proof-assistant software systems has potential of aiding the specification author in various aspects. We describe a study case in which the Isabelle/HOL language and the Isabelle proof-assistant environment are used to formalize a simplified version of the UFO-A ontology of endurants, to verify and correct the original axiomatization, and to optimize the specification theory's axioms and signature.
| Original language | English |
|---|---|
| Number of pages | 14 |
| Journal | CEUR workshop proceedings |
| Volume | 2969 |
| Publication status | Published - 2021 |
| Event | Joint Ontology Workshops, JOWO 2021: Episode VII: The Bolzano Summer of Knowledge - Bolzano, Italy Duration: 11 Sept 2021 → 18 Sept 2021 |
Keywords
- Applied ontology
- Formal methods
- Proof assistants
- Upper ontology
Fingerprint
Dive into the research topics of 'On the role of automated proof-assistants in the formalization of upper ontologies'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver