PreDeLo 1.0 is a theorem prover for preferential Description Logics. These are non monotonic extensions of standard DLs based on a typicality operator T, which enjoys a preferential semantics. PreDeLo 1.0 is a Prolog implementation of labelled tableaux calculi for such extensions, and it is able to deal with the preferential extension of the basic DL ALC as well as with the preferential extension of the lightweight DL DL-Litecore. The Prolog implementation is inspired by the “lean” methodology, whose basic idea is that each axiom or rule of the tableaux calculi is implemented by a Prolog clause of the program. Concerning ALC, PreDeLo 1.0 considers two extensions based, respectively, on Kraus, Lehmann and Magidor’s preferential and rational entailment.