DysToPic: a Multi-Engine Theorem Prover for Preferential Description Logics

We describe DysToPic, a theorem prover for the preferential De- scription Logic ALC + Tmin. This is a nonmonotonic extension of standard ALC based on a typicality operator T, which enjoys a preferential 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 performances of DysToPic are promis- ing,andsignificantlybetterthantheonesofitspredecessorPreDeLo 1.0.