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

Abstract. 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

• Type: Journal
• Year: 2015
• Where: AIIA
• Authors: Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato, Luca Violanti
• Keywords: AIIA 2015, Artificial Intelligence