Abstract We report on an implementation of a tableaux calculus for sceptical consequence in Default Logic built on Hybrid Modal Logic. In turn, our tool offers support for checking default consequence over formulas from Propositional Logic, Basic Modal Logic and Hybrid Logic. We develop a test suite for assessing the correctness, scalability, and efficiency of our system, and inform on the results. Interestingly, our method can be adapted to generate examples for other default provers.

Relation-changing modal logics are extensions of the basic modal logic with dynamic operators that modify the accessibility relation of a model during the evaluation of a formula.These languages are equipped with dynamic modalities that are able, for example, to delete, add, and swap edges in the model, both locally and globally.We study the satisfiability problem for some of these logics.We first show that they can be translated into hybrid logic.As a result, we can transfer some results from hybrid logics to relation-changing modal logics.We discuss in particular, decidability for some fragments.We then show that satisfiability is, in general, undecidable for all the languages introduced, via translations from memory logics.