Switch to: References

Citations of:

A simple propositional S5 tableau system

Annals of Pure and Applied Logic 96 (1-3):107-115 (1999)

Add citations

You must login to add citations.

Tautology Elimination, Cut Elimination, and S5.Andrezj Indrzejczak - 2017 - Logic and Logical Philosophy 26 (4):461-471.details Tautology elimination rule was successfully applied in automated deduction and recently considered in the framework of sequent calculi where it is provably equivalent to cut rule. In this paper we focus on the advantages of proving admissibility of tautology elimination rule instead of cut for sequent calculi. It seems that one may find simpler proofs of admissibility for tautology elimination than for cut admissibility. Moreover, one may prove its admissibility for some calculi where constructive proofs of cut admissibility fail. As (...) Download Export citation Bookmark 2 citations
A Deep Inference System for the Modal Logic S5.Phiniki Stouppa - 2007 - Studia Logica 85 (2):199-214.details We present a cut-admissible system for the modal logic S5 in a formalism that makes explicit and intensive use of deep inference. Deep inference is induced by the methods applied so far in conceptually pure systems for this logic. The system enjoys systematicity and modularity, two important properties that should be satisfied by modal systems. Furthermore, it enjoys a simple and direct design: the rules are few and the modal rules are in exact correspondence to the modal axioms. Download Export citation Bookmark 8 citations
Proof Theory for Modal Logic.Sara Negri - 2011 - Philosophy Compass 6 (8):523-538.details The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective. Download Export citation Bookmark 22 citations
Realizations and LP.Melvin Fitting - 2010 - Annals of Pure and Applied Logic 161 (3):368-387.details LP can be seen as a logic of knowledge with justifications. See [S. Artemov, The logic of justification, The Review of Symbolic Logic 1 477–513] for a recent comprehensive survey of justification logics generally. Artemov’s Realization Theorem says justifications can be extracted from validities in the more conventional Hintikka-style logic of knowledge S4, in which they are not explicitly present. Justifications, however, are far from unique. There are many ways of realizing each theorem of S4 in the logic LP. If (...) Download Export citation Bookmark 8 citations
Justification logic.Melvin Fitting - manuscriptdetails Download Export citation Bookmark 3 citations
Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus.Andrzej Indrzejczak - 2016 - Bulletin of the Section of Logic 45 (2).details In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to some 1-degree formula, i.e. a modally-flat formula with modal functors having only boolean formulas in its scope. In contrast to many sequent calculi for S5 the presented system does not introduce any extra devices. Thus it is a standard version of SC but (...) Download Export citation Bookmark 2 citations

1