Tableaux and hypersequents for justification logics (Q408538): Difference between revisions

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

zbMATH Keywords

justification logic

0 references

hypersequents

0 references

tableaux

0 references

modal logic

0 references

reviewed by

Grigori Mints

0 references

MaRDI profile type

MaRDI publication profile

0 references

full work available at URL

https://doi.org/10.1016/j.apal.2011.09.013

0 references

cites work

Explicit Provability and Constructive Semantics

0 references

Introducing Justification into Epistemic Logic

0 references

Q3837723

0 references

Q2751361

0 references

Proof methods for modal and intuitionistic logics

0 references

Logics With Several Modal Operators

0 references

Q4023115

0 references

Q2753601

0 references

Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems

0 references

Tableaux and Hypersequents for Justification Logic

0 references

On the complexity of the reflected logic of proofs

0 references

Single step tableaux for modal logics. Computational properties, complexity and methodology

0 references

Indexed systems of sequents and cut-elimination

0 references

Identifiers

zbMATH Open document ID

1239.03010

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

0 references

0 references

10.1016/J.APAL.2011.09.013

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:408538

@@ Property / DOI @@
-.1016/j.apal.2011.09.013
@@ Property / DOI: 10.1016/j.apal.2011.09.013 / rank @@
-Normal rank
@@ Property / review text @@
+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)].
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+B45
@@ Property / Mathematics Subject Classification ID: 03B45 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+B42
@@ Property / Mathematics Subject Classification ID: 03B42 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+F45
@@ Property / Mathematics Subject Classification ID: 03F45 / rank @@
+Normal rank
@@ Property / zbMATH DE Number @@
+6022769
@@ Property / zbMATH DE Number: 6022769 / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+justification logic
@@ Property / zbMATH Keywords: justification logic / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+hypersequents
@@ Property / zbMATH Keywords: hypersequents / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+tableaux
@@ Property / zbMATH Keywords: tableaux / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+modal logic
@@ Property / zbMATH Keywords: modal logic / rank @@
+Normal rank
@@ Property / reviewed by @@
+Grigori Mints
@@ Property / reviewed by: Grigori Mints / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.apal.2011.09.013
+Normal rank
@@ Property / OpenAlex ID @@
+W1981979308
@@ Property / OpenAlex ID: W1981979308 / rank @@
+Normal rank
@@ Property / cites work @@
+Explicit Provability and Constructive Semantics
@@ Property / cites work: Explicit Provability and Constructive Semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Introducing Justification into Epistemic Logic
@@ Property / cites work: Introducing Justification into Epistemic Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q3837723
@@ Property / cites work: Q3837723 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751361
@@ Property / cites work: Q2751361 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof methods for modal and intuitionistic logics
@@ Property / cites work: Proof methods for modal and intuitionistic logics / rank @@
+Normal rank
@@ Property / cites work @@
+Logics With Several Modal Operators
@@ Property / cites work: Logics With Several Modal Operators / rank @@
+Normal rank
@@ Property / cites work @@
+Q4023115
@@ Property / cites work: Q4023115 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2753601
@@ Property / cites work: Q2753601 / rank @@
+Normal rank
@@ Property / cites work @@
+Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
+Normal rank
@@ Property / cites work @@
+Tableaux and Hypersequents for Justification Logic
+Normal rank
@@ Property / cites work @@
+On the complexity of the reflected logic of proofs
+Normal rank
@@ Property / cites work @@
+Single step tableaux for modal logics. Computational properties, complexity and methodology
+Normal rank
@@ Property / cites work @@
+Indexed systems of sequents and cut-elimination
@@ Property / cites work: Indexed systems of sequents and cut-elimination / rank @@
+Normal rank
@@ Property / DOI @@
+.1016/J.APAL.2011.09.013
@@ Property / DOI: 10.1016/J.APAL.2011.09.013 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:408538