Rock type predicate definition. **The classification algorithm implicitly contains definitions of all types of igneous rock. Definitions can be obtained from**
the algorithm in the form of formulas one free variable formulas of predicate calculus of first order with numbers. The formula structure shows the complexity of the concept behind the term, and also specifies all the concepts **underlying**
a term. This is extremely important for finding the primary concepts. We have quite formally, i.e. using mathematical conversions, obtained formulas for the harzburgite and dunite predicates.

harzburgite: **when applied to the sample, the harzburgite predicate should**
give "true" if the sample is harzburgite, and "false" otherwise. Flowcharts have to be tracked from top to bottom, and conditions leading to a OOC diagram **field** flowchart node producing the "harzburgite" value collected, to get a predicate.

These conditions should be connected by the logical operation "and". The conversions will give the following formula:
harzburgite(x) = def plutonic(x) ∧ ¬ (pyroclastic(x) ∨ **kimberlite(x)**
∨ lamproite(x) ∨ lamprophyre(x) ∨ **charnockite(x))** ∧ VPC carbonates(x)≤ 50 ∧ VPC melilite(x)≤ 10 ∧ VPC **M(x)** ≥ 90 ∧ VPC kalsilite(x)=0 ∧ VPC leucite(x)=0 ∧ VPC **hornblende(x)=0**
∧ 0.4*VPC OOC(x)≤ VPC Ol(x)≤ 0.9*VPC **OOC(x)** ∧ VPC Cpx(x)<0.05*VPC **OOC(x)**
Thus, a precise definition of the harzburgite igneous rock type consists of three parts:
1. Qualitative characteristics (lines 1, 2). 2. Absolute restrictions on modal data (lines 3, 4).

3. Relative restrictions on modal data (lines 5, 6).

Now we can compare this definition with the informal definition quoted in Section 3: the formal definition is more complete. It does not suppose anything and does not refer to the diagram. It contains the necessary part of the diagram.

## 5 Lessons Learnt, What Is Next?

This paper describes our experience of converting the petrological information stored in databases, glossaries, and classification standards to a **formal OWLbased representation. A similar approach, i.e. one based on providing unambiguous and consistent definitions for all terms, can be used in developing a formal**
theory for virtually any scientific area. We will now briefly summarize the results and outline plans for the future.

From data to knowledge**. Moving from a database of petrological facts to a knowledge base is beneficial from multiple perspectives. Firstly, the new representation**
is richer and enables generation of sentences in a controlled natural language, which, in our experience, are understandable to geologists. They can be used not only as an interface to the KB, but also to annotate publications, which 8