Should I Stay or Should I Go - A New Reasoner for Description Logic.

We present the Emi reasoner, based on a new interpretation of the tableau algorithm for reasoning with Description Logics with unique performance characteristics and specialized advantages. Emi turns the tableau inside out, solving the satisfiability problem by adding elements to expressions rather than adding expressions to element node labels. This strategy is inspired by decidable reasoning algorithms for Horn Logics and that run on a loop rather than recursive graph-based strategies used in a tableau reasoner. Because Emi solves the same problem there will be a simple correspondence with tableaux, yet it will feel very different during execution, since the problem is inverted. This inversion makes possible many unique and straightforward optimizations, such as paralellization of many parts of the reasoning task, concurrent ABox expansion, and localized blocking techniques. Each of these optimizations contains a design trade-off that allows Emi to perform extremely well in certain cases, such as instance retrieval, and not as well in others. Our initial evaluations show that even a naive and largely un-optimized implementation of Emi is performant with popular reasoners running on the JVM such as Hermit, Pellet, and jFact.