OWL2.hs

{- |

The "OWL2" directory contains the OWL2 instance of "Logic.Logic".
The data for this instance is found in "OWL2.Logic_OWL2".

/Abstact Syntax/

The syntax for OWL2 is represented using Haskell datatypes. It is defined both in
OWL2.AS - which contains the entities and expressions (<http://www.w3.org/TR/owl2-syntax/>)
and in OWL2.MS - which contains the frames (<http://www.w3.org/TR/owl2-manchester-syntax/>).
As the official Manchester Syntax cannot express some of the valid OWL2 axioms,
the Haskell datatypes for frames were extended to also accomodate these.

/Parser/

The parsing of an OWL ontology happens in two main steps. First, the ontology is
converted to XML, using the Java parser found in "OWL2.java". Then, the XML is
parsed into the Haskell datatypes (see "OWL2.XML"). The top-level function which
combines the two steps is found in "OWL2.ParseOWLAsLibDefn".

The parser for the Het-CASL representation is found in "OWL2.Parse" and
"OWL2.ManchesterParser" which take as argument an ontology in our extended
Manchester Syntax and convert it into the Haskell datatypes.

/Pretty printing/

This is done in "OWL2.Print" (for the "AS.hs" datatypes) and in
"OWL2.ManchesterPrint" (fot the "MS.hs" datatypes). The output is written
in our extended Manchester Syntax.

A LaTeX output is not available, yet.

/Static Analysis/

The file "OWL2.StaticAnalysis" repairs the ontology after parsing and then
produces the final axioms and signature needed for hets analysis.

/Provers/

There are two of these for OWL2, namely Pellet and FACT++, written in Java.
The call for them happens in "OWL2.ProvePellet" and "OWL2.ProveFact". The input
for the provers is XML syntax, which comes from "OWL2.XMLConversion". The
conservativity check is implemented in "OWL2.Conservativity" and uses the Java-
written locality checker.

/Comorphisms/

There are three implemented comorphsims: from OWL2 to CASL and Common Logic
and from DMU to OWL2.

/Profiles and sublogics/

There are three OWL2 profiles: EL, QL and RL. In "OWL2.Profiles", an ontology
is taken as argument and analysed, in order to see in which of the profiles it
fits, while in "OWL2.Sublogics", the reasoning complexity of the ontology
is computed.

/Miscellaneous/

"OWL2.Function" provides a class for functions which go through all the Haskell
datatypes and which are structurally equivalent (except maybe on what they do
with the IRIs or entities). Currently, morphism mapping, prefix renaming
and IRI expansion are implemented there.

"OWL2.ColimSign" and "OWL2.Taxonomy" provide signature colimits and taxonomy
extraction, respectively.

-}

module OWL2 where