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

G. Hoffmann, C. Areces, V. Cassano, and R. Fervari. DefTab: A Tableaux System for Sceptical Consequence in Default Modal Logics. In R. Ramanayake and J. Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods, 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings, Lecture Notes in Computer Science, pp. 37–48, 2023.

Download

[pdf] 

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.

BibTeX

@InCollection{arec:deft23,
  author =       "G. Hoffmann and C. Areces and V. Cassano and R.
                 Fervari",
  editor = {R. Ramanayake and J. Urban},
  title =        "{DefTab}: {A} Tableaux System for Sceptical
                 Consequence in Default Modal Logics",
  booktitle =    "Automated Reasoning with Analytic Tableaux and Related Methods, 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings",
  year =         "2023",
  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.",
  pages = {37--48},
  series = {Lecture Notes in Computer Science},
  ISBN = {978-3-031-43512-6},
}