DysToPic: a Multi-Engine Theorem Prover for Preferential Description Logics
Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato, Luca Violanti · Institutional Research Information System University of Turin (University of Turin) · 2015
We describe DysToPic, a theorem prover for the preferential Description 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 promising, and significantly better than the ones of its predecessor PreDeLo 1.0.