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.
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.