On the Role of Automated Proof-Assistants in the Formalization of Upper Ontologies.
Joao Rafael Moraes Nicola, Giancarlo Guizzardi · University of Twente Research Information · 2021
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.