Introduction
------------

CEX2.5 is a tool for computing three types of logical differences between two 
acyclic ELHr terminologies, i.e. EL terminologies with additional domain
restrictions, range restrictions, and (simple) role inclusions. The types
of differences that can be analysed are differences w.r.t. concept inclusions,
answers to instance queries, and answers to conjunctive queries formulated over
a specified signature, which are logically entailed by a given terminology T1
but not by a second terminology T2.

CEX2.5 can compute a finite representation for each of the three difference
types described above by searching for so-called difference witnesses.
Additionally, CEX2.5 is also capable of finding example members of the
difference sets, i.e. concept inclusions (in an extended language), which
correspond to the difference witnesses. More details regarding the theoretical
background of CEX2.5 can be found in [1].

CEX2.5 makes use of the CB reasoner:

https://github.com/ykazakov/cb-reasoner/


Compilation Instructions
-------------------------

CEX2.5 is written in OCaml, i.e. it should be possible to compile it under any
architecture or operating system for which OCaml is available.

- Under Linux/Unix (where the 'make' tool is available) it should be sufficient
  to type 'make' in the 'src' directory in order to compile CEX2.5. The binary
  'cex25' will then also be created in the 'src' directory.

- On other operating systems the compilation can be initiated by typing

     ocamlbuild -lib unix -lib str -I cb/main -I cb/libs cex2.native

  in the 'src' directory. The resulting binary will then typically be called
  'cex2.native'.


Running CEX2.5
--------------

'cex25' can be run as follows

  cex25 --tbx1 <TBox1 file> --tbx2 <TBox2 file> --sig <signature file>
          --examples --mode concept --simplify

The input terminologies must be in KRSS format, and they are specified via the
'--tbx1' and '--tbx2' flags. The signature file is passed to CEX2.5 via the
'--sig' flag. It is also possible to use the full signature of either TBox1 or
TBox2, or their intersection as comparison signature by using the flag
'--use-sig' with either 'tbx1', 'tbx2', or 'shared' as arguments. If neither the
flags '--sig', nor '--use-sig' is given, then the full signature of TBox2 is
used.

Examples of input files for CEX2.5 can be found in the 'examples/' subdirectory.

The flag '--mode' with arguments 'concept', 'instance', or 'conjunctive-query'
('cq') can be used to switch either between the concept, instance or
conjunctive-query comparison mode, respectively.  By default concept
mode is selected.

The flag '--examples' activates the computation of members of either the
concept, instance, or conjunctive query difference sets that correspond to the
difference witnesses. By default only concept/role names are output together
with the information whether they are left-hand or right-hand difference
witnesses. Note that for examples illustrating instance queries or conjunctive
queries, CEX2.5 does not compute ABoxes or conjunctive queries directly, but
instead it outputs concept inclusions in ELHr extended with additional concept
constructors that capture the required expressivity of ABoxes or conjunctive
queries. More details regarding the translation between such concept inclusions
and ABoxes/conjunctive queries can be found in [1].

Finally, the flag '--simplify' switches on the simplification of the
constructed examples.

[1] Konev, B., Ludwig, M., Walther, D., Wolter, F.: The Logical Diff for the Lightweight
    Description Logic EL, available under http://www.csc.liv.ac.uk/~frank/publ/publ.html