Rule Refinement for Semantic Tableau Calculi

Dmitry Tishkovsky, Renate Schmidt

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


The paper investigates renement techniques for semantic
tableau calculi. The focus is on techniques to reduce branching in inference
rules and thus allow more eective ways of carring out deductions.
We introduce an easy to apply, general principle of atomic rule renement,
which depends on a purely syntactic condition that can be easily
veried. The renement has a wide scope, for example, it is immediately
applicable to inference rules associated with frame conditions of
modal logics, or declarations of role properties in description logics, and
it allows for routine development of hypertableau-like calculi for logics
with disjunction and negation. The techniques are illustrated on Humberstone's
modal logic Km(:) of `some', `all' and `only', for which two
rened calculi are derived.
Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods
Subtitle of host publication26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017 : proceedings
EditorsRenate A. Schmidt, Claudia Nalon
PublisherSpringer Nature
ISBN (Print)9783319669014
Publication statusPublished - 2017

Publication series

NameLecture Notes in Artificial Intelligence Series


Dive into the research topics of 'Rule Refinement for Semantic Tableau Calculi'. Together they form a unique fingerprint.

Cite this