Tableaux and hypersequents for justification logics (Q408538)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Tableaux and hypersequents for justification logics |
scientific article; zbMATH DE number 6022769
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Tableaux and hypersequents for justification logics |
scientific article; zbMATH DE number 6022769 |
Statements
Tableaux and hypersequents for justification logics (English)
0 references
10 April 2012
0 references
Logics of proofs (now called justification logics), introduced by S. Artemov, are usually based on S4. The author investigates a system S4LPN, introduced by S. Artemov and E. Nogina, which has an additional S5-like schema. He presents rather complicated tableau and hypersequent formulations for S4LPN. It is possible that a much more elegant formulation can be obtained using a cut-free system for S5 due to \textit{G. F. Shvarts} [``Gentzen style systems for K45 and K45D'', Lect. Notes Comput. Sci. 363, 245--256 (1989; Zbl 0677.03010)].
0 references
justification logic
0 references
hypersequents
0 references
tableaux
0 references
modal logic
0 references
0 references
0.877255916595459
0 references
0.8247348666191101
0 references
0.8143614530563354
0 references
0.7887142896652222
0 references
0.7847409844398499
0 references
