The DLP Experimental Description Logic System and Propositional Modal Logic Satisfiability Checker


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).

Version 3.3

Version 3.3 is the distributed version of the third major revision of DLP, with added expressive power over previous major versions. Version 3.3 has several optimisations and bug fixes over previous minor versions.

Version 4.1

Version 4.1 of DLP includes a number of changes from Version 3.3 of DLP, including new optimisations and compile-time options. This version incorporates dependency information needed in backjumping into the formula cache. It also optimizes the low-level computations, which used to be very expensive when many formulae were active. It can investigate modal successors before completing the current node and can often reuse the effort involved. It also incorporates a simple variant of dynamic backtracking.

Empirical Testing of DLP

DLP has been run on a number of test suites, and the results of this testing has been published in a number of papers about DLP.

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.

DLP Interfaces

DLP implements the description logic below, but it reads a larger fragment of the KRSS syntax (and ignores the parts it does not implement). Case is not significant in commands (``define-concept'', etc.) or in concept constructors that take arguments (``AND'', etc.) but it is significant in concept names and in concept constructors that look like names (``TOP'', ``BOTTOM'', ``NUMBER'').
<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:

  1. [in .]: a parser for a superset of the Tableaux'98 benchmarks
  2. [in ps]: two parsers for s-expressions, which are used for the PS random formulae, from files created by Ian Horrocks, and for some Galen formulae, from files created by Ian Horrocks;
  3. 3 [in dl]: a parser for part of the KRSS syntax as detailed above, which is used to load the Galen KB modified to be acceptable for KRIS.
To run any interface, just go to its directory, start SML, and type CM.make() to compile and load that interface for DLP. You then invoke the parser via
  1. Parser.process(<Tableaux'98 file>,<reflexive>,<transitive>,<largest>); where the arguments are the name of the file to load, whether to use a reflexive or transitive modal logic, and the largest formula to load (use 22 for all of them).
    <formula> ::= ~ <primary>
    | box <primary>
    | dia <primary>
    | <primary> & <primary>
    | <primary> v <primary>
    | <primary> -> <primary>
    | <primary> -> <primary>
    | <primary> <-> <primary>
    <primary> ::= true
    | false
    | p<digit>+
    | ( <formula> )
  2. PSParser.process(<PS file>,<statistics file>,<smallest formula >); where <PS file> is the name of a PS file, <statistics file> is the name of a file where statistics will be written, and <smallest formula size> says to skip formula smaller than this size.
  3. GKBParser.process(<GKB file>); where <GKB file> is the name of a file containing formulae.
    <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>*
  4. Parser.timeKB(<KB file>,<timeout>,<silent>); where <KB file> is the name of a DLP KB file, <timeout> is how many seconds to allow before aborting, and <silent> indicates whether to not print messages about the loading process.

For more information:

Write to Peter F. Patel-Schneider (pfps@research.bell-labs.com).


Updated November 2009 by Peter F. Patel-Schneider