Inverting subsumption for constructive reasoning

We present a Logic Programming prototype implementation, working as proof-of-concept for a unified strategy proposed in our past research to solve several non-standard reasoning problems in Description Logics (DLs), denoted by Constructive Reasoning. In order to prove both the problem-independence and the logic-independence of the adopted approach, the prototype is focused on the solution of three different problems - namely Least Common Subsumer, Concept Abduction and Concept Difference - and two different, though simple and endowed with structural subsumption, DLs, i.e., EL and ALN. Accordingly to the implemented strategy, problems are formalized as conjunction of both subsumption and non-subsumption statements, causing the whole prototype to rely on a Prolog program solving subsumption. The program is built around a predicate, which on the one hand checks for the existence of subsumption relations between ground elements, providing boolean answers, and on the other hand, if inverted, exploits Prolog built-in unification to enumerate variable values making subsumption true between concept terms containing concept variables.