Pronto: A Practical Probabilistic Description Logic Reasoner. This paper presents Pronto—the first probabilistic Description Logic (DL) reasoner capable of processing knowledge bases containing about a thousand of probabilistic axioms. We describe in detail the novel probabilistic satisfiability (PSAT) algorithm which lies at the heart of Pronto’s architecture. Its key difference from previously developed (propositional) PSAT algorithms is its interaction with the underlying DL reasoner which, first, enables applying well-known linear programming techniques to non-propositional PSAT and, second, is crucial to scaling with respect the amount of classical (non-probabilistic) knowledge. The latter is the key feature for dealing with probabilistic extensions of existing large ontologies. Finally we present the layered architecture of Pronto and demonstrate the experimental evaluation results on randomly generated instances of non-propositional PSAT.