Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents

2019 ◽  
pp. 185-202
Author(s):  
Rajeev Goré ◽  
Björn Lellmann
Keyword(s):  
Tense Logic ◽  
Cut Elimination ◽  
Proof Search ◽  
Nested Sequents

scholarly journals Focused Proof-search in the Logic of Bunched Implications

2021 ◽  
pp. 247-267
Author(s):  
Alexander Gheorghiu ◽  
Sonia Marin
Keyword(s):  
Data Structure ◽  
Proof Theory ◽  
Sequent Calculus ◽  
Operational Semantics ◽  
Search Space ◽  
Difficult Problem ◽  
Cut Elimination ◽  
Proof Search ◽  
Nested Sequents

AbstractThe logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can capture various goal-directed proof-search procedures. In this paper we show that focused proof-search is complete for BI by first reformulating the traditional bunched sequent calculus using the simpler data-structure of nested sequents, following with a polarised and focused variant that we show is sound and complete via a cut-elimination argument. This establishes an operational semantics for focused proof-search in the logic of Bunched Implications.

A Formally Verified Cut-Elimination Procedure for Linear Nested Sequents for Tense Logic

2021 ◽  
pp. 281-298
Author(s):  
Caitlin D’Abrera ◽  
Jeremy Dawson ◽  
Rajeev Goré
Keyword(s):  
Tense Logic ◽  
Cut Elimination ◽  
Elimination Procedure ◽  
Nested Sequents

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.

Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq

2021 ◽  
pp. 299-313
Author(s):  
Rajeev Goré ◽  
Revantha Ramanayake ◽  
Ian Shillito
Keyword(s):  
Cut Elimination ◽  
Provability Logic ◽  
Proof Search

scholarly journals Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity

2020 ◽  
Author(s):  
Tiziano Dalmonte ◽  
Björn Lellmann ◽  
Nicola Olivetti ◽  
Elaine Pimentel
Keyword(s):  
Search Strategy ◽  
Cut Elimination ◽  
Relational Semantics ◽  
Optimal Complexity ◽  
Proof Search ◽  
Polynomial Size ◽  
Hypersequent Calculi

Abstract We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms ${T}$, ${P}$ and ${D}$ and for every $n \geq 1$, rule ${RD}_n^+$. The calculi are internal as they only employ the language of the logic, plus additional structural connectives. We show that the calculi are complete with respect to the corresponding axiomatization by a syntactic proof of cut elimination. Then, we define a terminating proof search strategy in the hypersequent calculi and show that it is optimal for coNP-complete logics. Moreover, we show that from every failed proof of a formula or hypersequent it is possible to directly extract a countermodel of it in the bi-neighbourhood semantics of polynomial size for coNP logics, and for regular logics also in the relational semantics. We finish the paper by giving a translation between hypersequent rule applications and derivations in a labelled system for the classical cube.

scholarly journals Termination of derivations for minimal tense logic

2009 ◽  
Vol 50 ◽  
Author(s):  
Regimantas Pliuškevičius
Keyword(s):  
Tense Logic ◽  
Proof Search

It is known that loop checking and backtracking are extensively used in various non-classical logics. An efficient loop checking is obtained using a technique based on histories. In the paper a method for elimination of loop checking in backward proof search for minimal tense logic Kt is proposed. To obtain termination of derivation indices and marks are used instead of history.

Sign in / Sign up

Export Citation Format

Share Document