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 formally available for research and educational purposes, but the distribution mechanism is currently broken.
DLP can also be used as a satisfiability checker for various modal logics, including multi-modal versions of K and S4. It is one of the fastest satisfiability checkers for several modal logics. DLP handles transitive closure of modalities and was initially designed to handle all of PDL, but there are known bugs in DLP's handling of PDL.
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 (SML/NJ).
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> | |
<primary> ::= | true |
| false | |
| p<digit>+ | |
| ( <formula> ) |
<formula> ::= | <atom> |
| (AND <formula>+) | |
| (OR <formula>+) | |
| (NOT <formula>) | |
| (ALL <modal> <formula>) | |
| (SOME <modal> <formula>) | |
<modal> ::= | <atom> |
| (EITHER <modal>+) | |
| (COMPOSE <modal>+) | |
| (RESTRICT <formula>) | |
| (TRANSITIVE <modal>) | |
<atom> ::= | <alphabetic> <alphnumeric>* |