DefTab: A Tableaux System for Sceptical Consequence in Default Modal Logics

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.