TANCS-2000 Results for DLP

DLP [Patel-Schneider(1998)] is a description logic system that contains a sound and complete reasoner for expressive description logics. Due to the equivalences between expressive description logics and propositional modal logics, DLP can be used as a satisfiability checker for propositional modal logics, including K sub (m), KT sub (m), K4 sub (m), S4 sub (m), and PDL. DLP has performed very well in recent comparisons of modal provers {Horrocks and Patel-Schneider(1998a), Horrocks and Patel-Schneider(1998b)].