Sequent calculi and decidability for intuitionistic hybrid logic

被引：7

作者：

Galmiche, Didier ^{[1
]}

Salhi, Yakoub ^{[1
]}

机构：

[1] LORIA UHP Nancy 1, F-54506 Vandoeuvre Les Nancy, France

来源：

INFORMATION AND COMPUTATION | 2011年 / 209卷 / 12期

关键词：

Intuitionistic hybrid logic; Sequent calculus; Cut-elimination; Decidability;

D O I：

10.1016/j.ic.2011.10.002

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In this paper we study the proof theory of the first constructive version of hybrid logic called Intuitionistic Hybrid Logic (IHL) in order to prove its decidability. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for this logic. We prove its main properties like soundness, completeness and also the cut-elimination property. Finally we provide, from our calculus, the first decision procedure for IHL and then prove its decidability. (C) 2011 Elsevier Inc. All rights reserved.

引用

页码：1447 / 1463

页数：17

共 19 条

[1]

[Anonymous], MODAL LOGIC

[2]

[Anonymous], 2002, Cambridge Tracts in Theoretical Computer Science

[3]

[Anonymous], 2006, HDB MODAL LOGICS

[4]

[Anonymous], 1996, Cambridge Tracts Theor. Comput. Sci.

[5]

Areces C, 1999, LECT NOTES COMPUT SC, V1683, P307

[6] Internalizing labelled deduction [J].

Blackburn, P .

JOURNAL OF LOGIC AND COMPUTATION, 2000, 10 (01) :137-168

[7]

Bolander T., 2007, METHODS MODALITIES

[8]

Braüner T, 2004, J LOGIC COMPUT, V14, P229

[9]

Brauner Torben., 2006, J APPL LOGIC, V4, P231, DOI DOI 10.1016/J.JAL.2005.06.009

[10] A hybrid intuitionistic logic: Semantics and decidability [J].

Chadha, R ;

Macedonio, D ;

Sassone, V .

JOURNAL OF LOGIC AND COMPUTATION, 2006, 16 (01) :27-59

← 1 2 →