METTEL: A Tableau Prover with Logic-Independent Inference Engine

摘要

METTEL is a generic tableau prover for various modal, intuitionistic, hybrid, description and metric logics. The core component of METTEL is a logic-independent tableau inference engine. A novel feature is that users have the ability to flexibly specify the set of tableau rules to be used in derivations. Termination can be achieved via a generalisation of a standard loop checking mechanism or unrestricted blocking.