The most promiment ontology definition formalism is
OWL,
which is, in fact, three increasingly-expressive languages:
OWL Lite, which is equivalent to SHIF(D),
OWL-DL, which is equivalent to SHOIN(D), and
OWL Full, which is equivalent to a second-order logic.
Univ. of Manchester and and Univ. of Karlsruhe offer a variaty of
on-line
OWL tools:
an OWL Validator
that classifies OWL files as Lite, DL, Full, or invalid.
It also lists all logical constructs found in the file.
a Converter
between OWL and abstract DL syntax, lisp-like FaCT++ syntax,
DIG 2.0, or Prolog-like Theorem-Prover syntax.
a Presentation servlet
that prepares an HTML, javadoc-like presentation of the Ontology.
A newer specification
(OWL 1.1)
is under preparation, which will extend the admissible
relation descriptions to almost full RBox reasoning. OWL-DL 1.1 is
equivalent to the DL called SROIQ(D).