scholarly journals Efficient loop-check for multimodal KD45n logic

2021 ◽  
Vol 47 ◽  
Author(s):  
Adomas Birštunas
Keyword(s):  
Modal Logic ◽  
Sequent Calculus ◽  
Space Complexity ◽  
Maximum Height ◽  
Polynomial Space ◽  
Inference Rules ◽  
Derivation Tree ◽  
Modal Operator

We introduce sequent calculus for multi-modal logic KD45n which uses efficient loop-check. Efficiency of the used loop-check is obtained by using marked modal operator squarei which is used as an alternative to sequent with histories ([2,3]).We use inference rules with or branches to make all rules invertible or semi-invertible. We showthe maximum height of the constructed derivation tree.  Also polynomial space complexity is proved.

On finite and infinite modal systems

1938 ◽  
Vol 3 (2) ◽  
pp. 77-82 ◽  
Author(s):  
C. West Churchman
Keyword(s):  
Modal Logic ◽  
Symbolic Logic ◽  
Modal Operator ◽  
Image Position ◽  
Modal Systems ◽  
Complex Modal

In Oskar Becker's Zur Logik der Modalitäten four systems of modal logic are considered. Two of these are mentioned in Appendix II of Lewis and Langford's Symbolic logic. The first system is based on A1–8 plus the postulate,From A7: ∼◊p⊰∼p we can prove the converse of C11 by writing ∼◊p for p, and hence deriveThe addition of this postulate to A1–8, as Becker points out, allows us to “reduce” all complex modal functions to six, and these six are precisely those which Lewis mentions in his postulates and theorems: p, ∼p, ◊p, ∼◊p, ∼◊∼p, and ◊∼p This reduction is accomplished by showingwhere ◊n means that the modal operator ◊ is repeated n times; e.g., ◊3p = ◊◊◊p. Then it is shown thatBy means of (1), (2), and (3) any complex modal function whatsoever may be reduced to one of the six “simple” modals mentioned above.It might be asked whether this reduction could be carried out still further, i.e., whether two of the six “irreducible” modals could not be equated. But such a reduction would have to be based on the fact that ◊p = p which is inconsistent with the set B1–9 of Lewis and Langford's Symbolic logic and independent of the set A1–8. Hence for neither set would such a reduction be possible.

scholarly journals A general proof certification framework for modal logic

2019 ◽  
Vol 29 (8) ◽  
pp. 1344-1378
Author(s):  
TOMER LIBAL ◽  
MARCO VOLPE
Keyword(s):  
Modal Logic ◽  
General Framework ◽  
Sequent Calculus ◽  
Specification Language ◽  
Sequent Calculi ◽  
General Proof ◽  
Theorem Provers ◽  
Different Sources

One of the main issues in proof certification is that different theorem provers, even when designed for the same logic, tend to use different proof formalisms and produce outputs in different formats. The project ProofCert promotes the usage of a common specification language and of a small and trusted kernel in order to check proofs coming from different sources and for different logics. By relying on that idea and by using a classical focused sequent calculus as a kernel, we propose here a general framework for checking modal proofs. We present the implementation of the framework in a Prolog-like language and show how it is possible to specialize it in a simple and modular way in order to cover different proof formalisms, such as labelled systems, tableaux, sequent calculi and nested sequent calculi. We illustrate the method for the logic K by providing several examples and discuss how to further extend the approach.

PROOF SYSTEMS FOR VARIOUS FDE-BASED MODAL LOGICS

2019 ◽  
Vol 13 (4) ◽  
pp. 720-747
Author(s):  
SERGEY DROBYSHEVICH ◽  
HEINRICH WANSING
Keyword(s):  
Modal Logic ◽  
Sequent Calculus ◽  
Axiom System ◽  
Modal Logics ◽  
Cut Elimination ◽  
Proof Systems ◽  
Image Position ◽  
Axiomatic Extension

AbstractWe present novel proof systems for various FDE-based modal logics. Among the systems considered are a number of Belnapian modal logics introduced in Odintsov & Wansing (2010) and Odintsov & Wansing (2017), as well as the modal logic KN4 with strong implication introduced in Goble (2006). In particular, we provide a Hilbert-style axiom system for the logic $BK^{\square - } $ and characterize the logic BK as an axiomatic extension of the system $BK^{FS} $. For KN4 we provide both an FDE-style axiom system and a decidable sequent calculus for which a contraction elimination and a cut elimination result are shown.

Cut elimination and complexity bounds for intuitionistic epistemic logic

2020 ◽  
Vol 30 (1) ◽  
pp. 281-294
Author(s):  
Vladimir N Krupski
Keyword(s):  
Epistemic Logic ◽  
Sequent Calculus ◽  
Formal System ◽  
Point Of View ◽  
Cut Elimination ◽  
Polynomial Space ◽  
Complexity Bounds ◽  
Proof Search

Abstract The formal system of intuitionistic epistemic logic (IEL) was proposed by S. Artemov and T. Protopopescu. It provides the formal foundation for the study of knowledge from an intuitionistic point of view based on Brouwer–Heyting–Kolmogorov semantics of intuitionism. We construct a cut-free sequent calculus for IEL and establish that polynomial space is sufficient for the proof search in it. We prove that IEL is PSPACE-complete.

A proof-theoretic study of the correspondence of classical logic and modal logic

2003 ◽  
Vol 68 (4) ◽  
pp. 1403-1414 ◽  
Author(s):  
H. Kushida ◽  
M. Okada
Keyword(s):  
Modal Logic ◽  
Classical Logic ◽  
Predicate Logic ◽  
Transformation Method ◽  
Modal Operator ◽  
Theoretic Method ◽  
Barcan Formula ◽  
Theoretic Proof ◽  
Classical Predicate

AbstractIt is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; we investigate the correspondence between the quantified versions of S4 (with and without the Barcan formula) and the classical predicate logic (with one-sorted variable). We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof.

scholarly journals Loop-check elimination for non-transitive distributed knowledge logic

2008 ◽  
Vol 48 ◽  
Author(s):  
Aida Pliuškevičienė
Keyword(s):  
Modal Logic ◽  
Sequent Calculus ◽  
Distributed Knowledge ◽  
Knowledge Logic

A non-transitive distributed knowledge logic TnD, obtained from multi-modal logic Tn by adding distributed knowledge operator, is considered. Sound and complete loop-check-free sequent calculus for this logic is proposed. Termination of derivations in proposed calculus is justified.

scholarly journals A PURELY SYNTACTIC AND CUT-FREE SEQUENT CALCULUS FOR THE MODAL LOGIC OF PROVABILITY

2009 ◽  
Vol 2 (4) ◽  
pp. 593-611 ◽  
Author(s):  
FRANCESCA POGGIOLESI
Keyword(s):  
Modal Logic ◽  
Propositional Logic ◽  
Sequent Calculus ◽  
Semantic Element ◽  
Modal Propositional Logic

In this paper we present a sequent calculus for the modal propositional logic GL (the logic of provability) obtained by means of the tree-hypersequent method, a method in which the metalinguistic strength of hypersequents is improved, so that we can simulate trees shapes. We prove that this sequent calculus is sound and complete with respect to the Hilbert-style system GL, that it is contraction free and cut free and that its logical and modal rules are invertible. No explicit semantic element is used in the sequent calculus and all the results are proved in a purely syntactic way.

A cut-free labelled sequent calculus for dynamic epistemic logic

2020 ◽  
Vol 30 (1) ◽  
pp. 321-348
Author(s):  
Shoshin Nomura ◽  
Hiroakira Ono ◽  
Katsuhiko Sano
Keyword(s):  
Modal Logic ◽  
Epistemic Logic ◽  
Sequent Calculus ◽  
Dynamic Epistemic Logic ◽  
Kripke Semantics ◽  
Cut Rule ◽  
Public Announcement ◽  
Public Announcement Logic ◽  
Soundness And Completeness ◽  
Labelled Sequent Calculus

Abstract Dynamic epistemic logic is a logic that is aimed at formally expressing how a person’s knowledge changes. We provide a cut-free labelled sequent calculus ($\textbf{GDEL}$) on the background of existing studies of Hilbert-style axiomatization $\textbf{HDEL}$ of dynamic epistemic logic and labelled calculi for public announcement logic. We first show that the $cut$ rule is admissible in $\textbf{GDEL}$ and show that $\textbf{GDEL}$ is sound and complete for Kripke semantics. Moreover, we show that the basis of $\textbf{GDEL}$ is extended from modal logic K to other familiar modal logics including S5 with keeping the admissibility of cut, soundness and completeness.

Sign in / Sign up

Export Citation Format

Share Document