The Description Logic Prover (DLP) is an experimental description logic system, designed to investigate various options for checking satisfiability in expressive description logics and propositional modal logics. DLP is designed to allow various optimisations for description logic reasoning to be easily investigated. DLP is available for research and educational purposes. To obtain DLP, go to the Bell Labs software distribution site and request the DLP project.
DLP can also be used as a satisfiability checker for various modal logics. It is one of the fastest satisfiability checkers for several modal logics.
DLP is experimental because: 1/ there are only minimal interfaces; 2/ there is little optimization of the taxonomy code; and 3/ the code is written in ML in a mostly-functional style. Nevertheless, DLP is very fast under various sorts of measurements, and could be used for prototypes. The biggest lack of DLP is that it does not handle individuals.
DLP is written in Standard ML of New Jersey, which is available from Bell Labs.
The most recent set of tests employ a new generator for random CNF formulae in Km. The generator for these tests is included in DLP Version 4.1. The control files and results of these tests can be downloaded.
|<Concept> :: =||<TOP | BOTTOM | NUMBER | <Concept Name> ||
|(AND <Concept>*) ||
|(OR <Concept>*) ||
|(NOT <Concept>) ||
|(ALL <Role> <Concept>) ||
|(SOME <Role>) ||
|(NONE <Role>) ||
|(AT-LEAST <Integer> <Role>) ||
|(AT-MOST <Integer> <Role>) ||
|(EXACTLY <Integer> <Role>) ||
|(SOME <Role> <Concept>)|
|<Role> ::=||<Role Name>|
|<Statement> :: =||(define-concept <Concept Name> <Concept>) ||
|(define-primitive-concept <Concept Name> <Concept>) ||
|(define-primitive-role <Role Name>) ||
|(define-primitive-attribute <Role Name>) ||
|(concept-subsumes? <Concept> <Concept>)|
|<Knowledge Base> ::=||<Statement>*|
Note that DLP does not handle recursive definitions. A concept has to be defined BEFORE it is mentioned in the definition of a concept, including itself.
DLP has a large number of COMPILE-TIME options, as given in the file ``options.sml''.
The sources for dlp has several subdirectories: The satisfiability code is in the top directory. The taxonomy code is in the subdirectory dl. There are currently several interfaces:
|<formula> ::=||~ <primary>|
|| box <primary>|
|| dia <primary>|
|| <primary> & <primary>|
|| <primary> v <primary>|
|| <primary> -> <primary>|
|| <primary> -> <primary>|
|| <primary> <-> <primary>|
|| ( <formula> )|
|| (AND <formula>+)|
|| (OR <formula>+)|
|| (NOT <formula>)|
|| (ALL <modal> <formula>)|
|| (SOME <modal> <formula>)|
|| (EITHER <modal>+)|
|| (COMPOSE <modal>+)|
|| (RESTRICT <formula>)|
|| (TRANSITIVE <modal>)|
|<atom> ::=||<alphabetic> <alphnumeric>*|
|Tableaux 2000||Fabio Massacci||Source||http://www.dis.uniroma1.it/~tancs/|