TRILL

TRILL answers queries to SHOIQ knowledge bases using a tableau algorithm. Prolog non-determinism is used for easily handling non-deterministic expansion rules that produce more than one tableau.

You can try it online at http://trill-sw.eu/

Please, visit http://ml.unife.it/trill-framework/