MRG home page · Research · Publications · Projects · Software · People

Proof Guided Ontology Development

We propose a method of developing ontologies guided by attempted proofs of formally stated requirements for the ontologies.


Ontologies are (formal) models of some aspect of the real world (usually referred to as a domain), with applications such as information sharing, semantic search and interoperability; there are various ontologies in use, including many business and biomedical ones.


Building (and maintaining) such ontologies involves many activities, sources of knowledge and people; over the years these were analysed, organised and developed into methodologies, describing the whole process of building an ontology.

One idea used by several methodologies is the use of competency questions; these are questions that the ontology should be able to answer given some usage scenarios for it. An example for an e-Commerce ontology might be `what sequence of activities must be completed for an online purchase?'. These questions and their answers are then used to extract the main concepts, their properties, relations and axioms of the ontology. Usually, the finished ontology is evaluated to check that they are able to answer the questions.

Proof Guided Development

Sometimes the competency questions are formalised as logical statements and proved to follow from the (formal) ontology; if the latter is seen as a set of axioms, the former are theorems deducible from them. We believe proof attempts of formally stated requirements such as formalised competency questions could in fact be used to guide the ontology building process. That is, we start with the formal requirements statements and possibly a partial ontology, and use them to guide the user the relevant classes, relations and rules to add to the ontology so that it reflects the user's view of the domain at the same time as giving proofs of the statements.


Proof Guided Ontology Development: an overview of the project (pdf)


Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
Please send corrections and suggestions for this page to the DReaM Support Team
Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.