Labeled sequent calculi for modal logics and implicit contractions (Q377468): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(6 intermediate revisions by 5 users not shown) | |||
Property / review text | |||
The author investigates an issue directly concerning Negri's labeled sequent calculi, see [\textit{S. Negri}, J. Philos. Log. 34, No. 5--6, 507--544 (2005; Zbl 1086.03045)], based on Kleene's G3-style calculi [\textit{S. C. Kleene}, Introduction to metamathematics. Amsterdam: North-Holland Publishing Co. (1952; Zbl 0047.00703)] related to the standard modal systems K, D, T, K4, S4 and S5. The main result is that labeled calculi for the modal logics K and D remain complete w.r.t. valid tree-labeled sequents, that is, valid sequents whose relational part encodes a tree-like (not necessarily rooted) structure. The result is obtained when the unique rule containing a harmful implicit contraction is modified into a contraction-free one making the proof-search space finite. | |||
Property / review text: The author investigates an issue directly concerning Negri's labeled sequent calculi, see [\textit{S. Negri}, J. Philos. Log. 34, No. 5--6, 507--544 (2005; Zbl 1086.03045)], based on Kleene's G3-style calculi [\textit{S. C. Kleene}, Introduction to metamathematics. Amsterdam: North-Holland Publishing Co. (1952; Zbl 0047.00703)] related to the standard modal systems K, D, T, K4, S4 and S5. The main result is that labeled calculi for the modal logics K and D remain complete w.r.t. valid tree-labeled sequents, that is, valid sequents whose relational part encodes a tree-like (not necessarily rooted) structure. The result is obtained when the unique rule containing a harmful implicit contraction is modified into a contraction-free one making the proof-search space finite. / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B45 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F03 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 6223051 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
labeled sequent calculi | |||
Property / zbMATH Keywords: labeled sequent calculi / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
modal logics | |||
Property / zbMATH Keywords: modal logics / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
Kripke semantics | |||
Property / zbMATH Keywords: Kripke semantics / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
contraction rule | |||
Property / zbMATH Keywords: contraction rule / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Branislav R. Boričić / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/s00153-013-0350-y / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2040634330 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Deep sequent systems for modal logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Tableau methods of proof for modal logics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Proof methods for modal and intuitionistic logics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3408862 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Prefixed tableaus and nested sequents / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4894942 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q2753601 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A contraction-free and cut-free sequent calculus for propositional dynamic logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The Church-Fitch knowability paradox in the light of structural proof theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Strongly analytic tableaux for normal modal logics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Contraction-free sequent calculi for geometric theories with an application to Barr's theorem / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Proof analysis in modal logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Proof analysis in intermediate logics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Gentzen calculi for modal propositional logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4530621 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Displaying modal logic / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 01:05, 7 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Labeled sequent calculi for modal logics and implicit contractions |
scientific article |
Statements
Labeled sequent calculi for modal logics and implicit contractions (English)
0 references
6 November 2013
0 references
The author investigates an issue directly concerning Negri's labeled sequent calculi, see [\textit{S. Negri}, J. Philos. Log. 34, No. 5--6, 507--544 (2005; Zbl 1086.03045)], based on Kleene's G3-style calculi [\textit{S. C. Kleene}, Introduction to metamathematics. Amsterdam: North-Holland Publishing Co. (1952; Zbl 0047.00703)] related to the standard modal systems K, D, T, K4, S4 and S5. The main result is that labeled calculi for the modal logics K and D remain complete w.r.t. valid tree-labeled sequents, that is, valid sequents whose relational part encodes a tree-like (not necessarily rooted) structure. The result is obtained when the unique rule containing a harmful implicit contraction is modified into a contraction-free one making the proof-search space finite.
0 references
labeled sequent calculi
0 references
modal logics
0 references
Kripke semantics
0 references
contraction rule
0 references
0 references