Focused Proof-search in the Logic of Bunched Implications

Lecture Notes in Computer Science - Foundations of Software Science and Computation Structures ◽

10.1007/978-3-030-71995-1_13 ◽

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.

Download Full-text

Cut elimination and complexity bounds for intuitionistic epistemic logic

Journal of Logic and Computation ◽

10.1093/logcom/exaa012 ◽

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.

Download Full-text

A labelled sequent calculus for BBI: proof theory and proof search

Journal of Logic and Computation ◽

10.1093/logcom/exv033 ◽

2015 ◽

Vol 28 (4) ◽

pp. 809-872

Author(s):

Zhé Hóu ◽

Rajeev Goré ◽

Alwen Tiu

Keyword(s):

Proof Theory ◽

Sequent Calculus ◽

Proof Search ◽

Labelled Sequent Calculus

Download Full-text

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

Lecture Notes in Computer Science - Automated Reasoning with Analytic Tableaux and Related Methods ◽

10.1007/978-3-030-29026-9_11 ◽

2019 ◽

pp. 185-202

Author(s):

Rajeev Goré ◽

Björn Lellmann

Keyword(s):

Tense Logic ◽

Cut Elimination ◽

Proof Search ◽

Nested Sequents

Download Full-text

A contribution to automated-oriented reasoning about permutability of sequent calculi rules

Computer Science and Information Systems ◽

10.2298/csis120820043l ◽

2013 ◽

Vol 10 (3) ◽

pp. 1185-1210 ◽

Cited By ~ 1

Author(s):

Tatjana Lutovac ◽

James Harland

Keyword(s):

Proof Theory ◽

Sequent Calculus ◽

Sufficient Conditions ◽

General Treatment ◽

Cut Elimination ◽

Sequent Calculi ◽

Special Cases ◽

Necessary And Sufficient ◽

Different Parts ◽

Sequence Rules

Many important results in proof theory for sequent calculus (cut-elimination, completeness and other properties of search strategies, etc) are proved using permutations of sequent rules. The focus of this paper is on the development of systematic and automated-oriented techniques for the analysis of permutability in some sequent calculi. A representation of sequent calculi rules is discussed, which involves greater precision than previous approaches, and allows for correspondingly more precise and more general treatment of permutations. We define necessary and sufficient conditions for the permutation of sequence rules. These conditions are specified as constraints between the multisets that constitute different parts of the sequent rules. The authors extend their previous work in this direction to include some special cases of permutations.

Download Full-text

A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search

Lecture Notes in Computer Science - Automated Reasoning with Analytic Tableaux and Related Methods ◽

10.1007/978-3-642-40537-2_16 ◽

2013 ◽

pp. 172-187 ◽

Cited By ~ 8

Author(s):

Zhé Hóu ◽

Alwen Tiu ◽

Rajeev Goré

Keyword(s):

Proof Theory ◽

Sequent Calculus ◽

Proof Search ◽

Labelled Sequent Calculus

Download Full-text

PROOF-THEORETIC ANALYSIS OF THE QUANTIFIED ARGUMENT CALCULUS

The Review of Symbolic Logic ◽

10.1017/s1755020318000114 ◽

2019 ◽

Vol 12 (4) ◽

pp. 607-636 ◽

Cited By ~ 1

Author(s):

EDI PAVLOVIĆ ◽

NORBERT GRATZL

Keyword(s):

Proof Theory ◽

Natural Deduction ◽

Sequent Calculus ◽

Cut Elimination ◽

Theoretic Analysis ◽

Subformula Property

AbstractThis article investigates the proof theory of the Quantified Argument Calculus (Quarc) as developed and systematically studied by Hanoch Ben-Yami [3, 4]. Ben-Yami makes use of natural deduction (Suppes-Lemmon style), we, however, have chosen a sequent calculus presentation, which allows for the proofs of a multitude of significant meta-theoretic results with minor modifications to the Gentzen’s original framework, i.e., LK. As will be made clear in course of the article LK-Quarc will enjoy cut elimination and its corollaries (including subformula property and thus consistency).

Download Full-text