Rule Refinement for Semantic Tableau Calculi

Tishkovsky, D. and Schmidt, R. A. (2017)

In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017). Springer. Lecture Notes in Artificial Intelligence, Vol. 10501, Springer, 228-244. BiBTeX, PDF, (final version available via DOI link to Springer).

This paper investigates refinement techniques for semantic tableau calculi. The focus is on techniques to reduce branching in inference rules and thus allow more effective ways of carrying out deductions. We introduce an easy to apply, general principle of atomic rule refinement, which depends on a purely syntactic condition that can be easily verified. The refinement 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(not) with modal operators defined with respect to both accessibility and inaccessibility, for which two refined calculi are given.

Long version.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 12 Dec 17
Copyright © 2017 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk