EL+SAT (2014 edition)

EL+SAT is an automated-reasoning tool for concept subsumption and axiom pinpointing in Description logic EL+ based on Horn-SAT encoding, Conflict Analysis and ALL-SMT technology, which is described in the papers: The information related to the "old" CADE-22 version of EL+SAT (executables, data) can be downloaded here.

For JAIR reviewers' convenience, we report here the tools, data and encodings used in the JAIR-submitted paper above:

or, alternatively: Notice that the tarballs contain a modified version of the code of the Minisat 2.0. SAT solver.

IMPORTANT REMARK #1:
Due to licence issues, the tarball(s) above cannot contain the SNOMED ontology, neither the original version nor our own encoding, because the SNOMED ontology was gently provided to us by IHTSDO under a non-disclosure agreement, so that we are not authorized to make it available in any form. Whoever is willing to obtain an academic-licenced version, from which the encoding can be produced with our tool, is supposed to ask it to IHTSDO, as we did.
The other ontologies not-GALEN, full-GALEN, NCI, GENEONTOLOGY which have been used in the empirical evaluation of this paper, instead, can be freely downloaded at this link; they and their encodings can be found in the tarballs above.

IMPORTANT REMARK #2:
Before the end of the review process of the JAIR submission mentioned above, the tools, data and encodings above are made available for and only for the JAIR reviewers' convenience to help their reviewing process. No other usage from anybody is admitted without the explicit authorization from the authors (R. Sebastiani and Michele Vescovi).

Maintained by Roberto Sebastiani, rseba@disi.unitn.it.