System Description: DLP

DLP (Description Logic Prover) is an experimental description logic knowledge representation system. DLP implements an expressive description logic that includes propositional dynamic logic as a subset. DLP provides a simple interface allowing users to build knowledge bases of descriptions in this description logic, but, as an experimental system, DLP does not have a full user interface. Because of the correspondence between description logics and propositional modal logics, the description logic reasoner in CLP can serve as a reasoner for several propositional modal logics. As well as propositional dynamic logic, the logic underlying DLP contains fragments that are in direct correspondence to the propositional modal logics K sub (m). DLP provides an interface that allows direct satisfiability checking of formulae in K sub (m) and K4 sub (m). Using a standard encoding, the interface also allows satisfiability checking of formulae in KT sub (m) and S4 sub (m).