A Multi-Engine Theorem Prover for a Description Logic of Typicality

We describe DysToPic, a theorem prover for the preferen- tial Description Logic ALC + Tmin .This is a nonmonotonic extension of standard ALC based on a typicality operator T, which enjoys a prefer- ential semantics. DysToPic is a multi-engine Prolog implementation of a labelled, two-phase tableaux calculus for ALC + Tmin whose basic idea is that of performing these two phases by different machines. The per- formances of DysToPic are promising, and significantly better than the ones of its predecessor PreDeLo 1.0 recently introduced.