MLTP

MLTP is a modal logic tableau prover inplemented by Zhen Li.

MLTP implements a labelled tableau calculus, aiming to maximize both efficiency and generality. Several optimization techniques for modal logic reasoning are incorporated in MLTP. These include backjumping, dynamic backtracking, and forward reasoning. Forward reasoning consists of two techniques, forward checking and forward implication. Simplification is also implemented to remove redundancy. Among these optimization techniques advanced backtracking methods have proved to be most effective. Evaluation results show that dynamic backtracking improves the performance significantly. The effectiveness of forward checking is less marked however and needs to be investigated further.

To facilitate generic reasoning, MLTP incorporates a generic data structure, a low-level macro language, an event-handler framework and a high-level specification language. The generic data structure stores data and its relations in highly connected relation-based structures to provide different kinds of data processing in a uniform way. The low-level macro language uses a small set of standard instructions to perform complicated operations. The event-handler framework divides the system into loosely connected modules. Each module can be defined using the low-level macro language, whereas the pairing of events and handlers is controlled by the high-level specification language. The high-level specification language can be used to specify the syntax and grammar of the logics, the inference rules to be used and the strategies of the prover.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified:
Copyright © 1999-2009 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk