Rule Refinement for Semantic Tableau Calculi

Dmitry Tishkovsky; Renate Schmidt

doi:10.1007/978-3-319-66902-1_14

Rule Refinement for Semantic Tableau Calculi

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

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 language	English
Title of host publication	Automated Reasoning with Analytic Tableaux and Related Methods
Subtitle of host publication	26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017 : proceedings
Editors	Renate A. Schmidt, Claudia Nalon
Publisher	Springer Nature
Pages	228-244
Volume	10501
ISBN (Print)	9783319669014
DOIs	https://doi.org/10.1007/978-3-319-66902-1_14
Publication status	Published - 2017

Publication series

Name	Lecture Notes in Artificial Intelligence Series
Volume	10501

Access to Document

10.1007/978-3-319-66902-1_14Licence: CC BY

Cite this

Tishkovsky, D., & Schmidt, R. (2017). Rule Refinement for Semantic Tableau Calculi. In R. A. Schmidt, & C. Nalon (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017 : proceedings (Vol. 10501, pp. 228-244). (Lecture Notes in Artificial Intelligence Series ; Vol. 10501). Springer Nature. https://doi.org/10.1007/978-3-319-66902-1_14

Tishkovsky, Dmitry ; Schmidt, Renate. / Rule Refinement for Semantic Tableau Calculi. Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017 : proceedings . editor / Renate A. Schmidt ; Claudia Nalon. Vol. 10501 Springer Nature, 2017. pp. 228-244 (Lecture Notes in Artificial Intelligence Series ).

@inproceedings{a5d583d0d9344e1eb1a9578f941669b2,

title = "Rule Refinement for Semantic Tableau Calculi",

abstract = "The paper investigates renement techniques for semantictableau calculi. The focus is on techniques to reduce branching in inferencerules 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 easilyveried. The renement has a wide scope, for example, it is immediatelyapplicable to inference rules associated with frame conditions ofmodal logics, or declarations of role properties in description logics, andit allows for routine development of hypertableau-like calculi for logicswith disjunction and negation. The techniques are illustrated on Humberstone'smodal logic Km(:) of `some', `all' and `only', for which tworened calculi are derived.",

author = "Dmitry Tishkovsky and Renate Schmidt",

note = "This research was supported by UK EPSRC research grant EP/H043748/1.",

year = "2017",

doi = "10.1007/978-3-319-66902-1_14",

language = "English",

isbn = "9783319669014",

volume = "10501",

series = "Lecture Notes in Artificial Intelligence Series ",

publisher = "Springer Nature",

pages = "228--244",

editor = "Schmidt, {Renate A.} and Nalon, {Claudia }",

booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods",

address = "United States",

}

Tishkovsky, D & Schmidt, R 2017, Rule Refinement for Semantic Tableau Calculi. in RA Schmidt & C Nalon (eds), Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017 : proceedings . vol. 10501, Lecture Notes in Artificial Intelligence Series , vol. 10501, Springer Nature, pp. 228-244. https://doi.org/10.1007/978-3-319-66902-1_14

Rule Refinement for Semantic Tableau Calculi. / Tishkovsky, Dmitry; Schmidt, Renate.
Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017 : proceedings . ed. / Renate A. Schmidt; Claudia Nalon. Vol. 10501 Springer Nature, 2017. p. 228-244 (Lecture Notes in Artificial Intelligence Series ; Vol. 10501).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Rule Refinement for Semantic Tableau Calculi

AU - Tishkovsky, Dmitry

AU - Schmidt, Renate

N1 - This research was supported by UK EPSRC research grant EP/H043748/1.

PY - 2017

Y1 - 2017

N2 - The paper investigates renement techniques for semantictableau calculi. The focus is on techniques to reduce branching in inferencerules 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 easilyveried. The renement has a wide scope, for example, it is immediatelyapplicable to inference rules associated with frame conditions ofmodal logics, or declarations of role properties in description logics, andit allows for routine development of hypertableau-like calculi for logicswith disjunction and negation. The techniques are illustrated on Humberstone'smodal logic Km(:) of `some', `all' and `only', for which tworened calculi are derived.

AB - The paper investigates renement techniques for semantictableau calculi. The focus is on techniques to reduce branching in inferencerules 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 easilyveried. The renement has a wide scope, for example, it is immediatelyapplicable to inference rules associated with frame conditions ofmodal logics, or declarations of role properties in description logics, andit allows for routine development of hypertableau-like calculi for logicswith disjunction and negation. The techniques are illustrated on Humberstone'smodal logic Km(:) of `some', `all' and `only', for which tworened calculi are derived.

U2 - 10.1007/978-3-319-66902-1_14

DO - 10.1007/978-3-319-66902-1_14

M3 - Conference contribution

SN - 9783319669014

VL - 10501

T3 - Lecture Notes in Artificial Intelligence Series

SP - 228

EP - 244

BT - Automated Reasoning with Analytic Tableaux and Related Methods

A2 - Schmidt, Renate A.

A2 - Nalon, Claudia

PB - Springer Nature

ER -

Tishkovsky D, Schmidt R. Rule Refinement for Semantic Tableau Calculi. In Schmidt RA, Nalon C, editors, Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017 : proceedings . Vol. 10501. Springer Nature. 2017. p. 228-244. (Lecture Notes in Artificial Intelligence Series ). Epub 2017 Aug 30. doi: 10.1007/978-3-319-66902-1_14

Rule Refinement for Semantic Tableau Calculi

Abstract

Publication series

Access to Document

Fingerprint

Cite this