Alex, We have to make a clear distinction of (1) Historical developments, (2) Particular implementations, (3) Logical foundations, (4) Practical usage and development. Alex: Description Logic is a theoretic basis for OWL2 - the most used formal language for ontologies. If we consider point #1, the type hierarchy for DLs was specified by Aristotle with his syllogisms, which are more readable today than any current implementation of OWL (Point #2). There are four rules (A I E O), which can be expressed in Greek, English, or any other natural language. These rules have been widely used for centuries, and they are a highly readable notation for the OWL hierarchy: A: Every S is P. (S is the subject, and P is the predicate) I: Some S is P. E; No S is P, O: Some S is not P. For an introduction and examples, see slides 25 to 30 of https://jfsowa.com/talks/patolog1.pdf . For theoretical issues (Point #3), see slides 26 to 33. The Stoic logicians introduced Greek sentence patterns (#2 and #3) for assertions in a subset of first-order logic. In the 14th century, Ockham introduced a more complete range of sentence patterns in Latin that could represent the full expressive power of first-order logic (#3 and #4). His notation was very readable (by anyone who could read Latin or its translation to English and other languages). But he didn't have all the reasoning methods of modern FOL for proving the expressive power. In addition to the type hierarchy, Brachman and Fikes (1979) wrote a paper about KL-ONE (Knowledge Language 1), which consisted of a terminology (T-Box) for the equivalent of Aristotle's syllogisms, and a notation for assertions (A-Box). This covers points #1, #2, #3, and #4 as a superset of OWL4. Anything and everything that can be represented in OWL2 can be represented in KL-ONE, or in Latin according to Ockham's Summa Logicae. But the Greek and Latin versions or their translation to modern languages had the same advantage as KL-ONE: The full expressive power of first-order logic. And by the way, C. S. Peirce was familiar with all the logic methods by the ancient Greeks and the medieval Latins. He took pride in having the largest collection of medieval manuscripts on logic in the Boston area (which included the Harvard libraries). When he specified his versions of logic, he was familiar with all the earlier options. By comparison, however, OWL2 was a major step BACKWARDS from the Greeks, the Latins, and KL-ONE by the hopelessly misguided idea that decidabiity was important. It just made the notation more complex, harder to read, harder to write, harder to implement, and much less expressive. Recommendation for OWL3: An upward compatible version that allows any statements in Turtle or other notations plus any statements in pure and simple first-order logic. That means that all current implementations can continue to be used without change. The user notation can be a highly readable controlled natural language, such as ACE. This gives us the best of all options #1, #2, #3, and #4 -- plus upward compatibility with current implementations. John PS: Since the word 'sowa' means owl in Polish, this version of OWL3 would rescue my totem animal from the ignominy of a horrible version of logic. That's another plus. ---------------------------------------- From: "Alex Shkotin" <alex.shkotin(a)gmail.com> John, Description Logic is a theoretic basis for OWL2 - the most used formal language for ontologies. And at the very beginning they distinguished theoretical and factological (aka structural) propositions. Axioms and assertions in their terminology. What we need on the way to formal theoretical knowledge is a pattern for formal definitions and formal proofs. Like this here definition