Switch to: Citations

References in:

Tableaux and hypersequents for justification logics

Hidenori Kurokawa

Annals of Pure and Applied Logic 163 (7):831-853 (2012)

Add references

You must login to add references.

Indexed systems of sequents and cut-elimination.Grigori Mints - 1997 - Journal of Philosophical Logic 26 (6):671-696.details Cut reductions are defined for a Kripke-style formulation of modal logic in terms of indexed systems of sequents. A detailed proof of the normalization (cutelimination) theorem is given. The proof is uniform for the propositional modal systems with all combinations of reflexivity, symmetry and transitivity for the accessibility relation. Some new transformations of derivations (compared to standard sequent formulations) are needed, and some additional properties are to be checked. The display formulations [1] of the systems considered can be presented as (...) Download Export citation Bookmark 24 citations
Logic of proofs and provability.Tatiana Yavorskaya - 2001 - Annals of Pure and Applied Logic 113 (1-3):345-372.details In the paper the joint Logic of Proofs and Provability is presented that incorporates both the modality □ for provability 287–304) and the proof operator tF representing the proof predicate “t is a proof of F” . The obtained system naturally includes both the modal logic of provability GL and Artemov's Logic of Proofs . The presence of the modality □ requires two new operations on proofs that together with operations of allow to realize all the invariant operations on proofs (...) Download Export citation Bookmark 6 citations
Explicit provability and constructive semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.details In 1933 Godel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which (...) Download Export citation Bookmark 116 citations
The method of hypersequents in the proof theory of propositional non-classical logics.Arnon Avron - 1977 - In Wilfrid Hodges (ed.), Logic. New York: Penguin Books. pp. 1-32.details Until not too many years ago, all logics except classical logic (and, perhaps, intuitionistic logic too) were considered to be things esoteric. Today this state of a airs seems to have completely been changed. There is a growing interest in many types of nonclassical logics: modal and temporal logics, substructural logics, paraconsistent logics, non-monotonic logics { the list is long. The diversity of systems that have been proposed and studied is so great that a need is felt by many researchers (...) Download Export citation Bookmark 59 citations
Tableaux and hypersequents for justification logics.Hidenori Kurokawa - 2012 - Annals of Pure and Applied Logic 163 (7):831-853.details Download Export citation Bookmark 4 citations
Epistemic completeness of GLA.E. Nogina - 2007 - Bulletin of Symbolic Logic 13 (3):407.details Download Export citation Bookmark 4 citations

1