LotrecScheme

We propose a generic tableau prover extending Lotrec, called LotrecScheme: the tool enables to enrich tableau method rules with executable code. The user can graphically design its own tableau method and can solve the problem of model construction. This new system provides a way to merge two worlds when the system check a loop (for instance for S4): merging instead of blocking has the benefit of providing a real model and not just a skeleton of the model. The system generalizes also the notion of satisfiability to labeled graphs.