AI*IA 2015 Advances in Artificial Intelligence

We describe DysToPic, a theorem prover for the preferential Description Logic \(\mathcal {ALC}+\mathbf{T}_{min}\).This is a nonmonotonic extension of standard \(\mathcal {ALC}\) based on a typicality operator \(\mathbf{T}\), which enjoys a preferential semantics. DysToPic is a multi-engine Prolog implementation of a labelled, two-phase tableaux calculus for \(\mathcal {ALC}+\mathbf{T}_{min}\) whose basic idea is that of performing these two phases by different machines. The performances of DysToPic are promising, and significantly better than the ones of its predecessor PreDeLo 1.0 recently introduced.