Cut-elimination for SBL
Logic
2016-06-15 v1
Authors:
Toshiyasu Arai
Abstract
In this paper we give a terminating cut-elimination procedure for a logic calculus SBL. SBL corresponds to the second order arithmetic Pi^{1}_{2}-Separation and Bar Induction.
Cite
@article{arxiv.1606.04194,
title = {Cut-elimination for SBL},
author = {Toshiyasu Arai},
journal= {arXiv preprint arXiv:1606.04194},
year = {2016}
}
Related papers
View all related →
Logic in Computer Science · Computer Science
A theory of cut-restriction: first steps
Agata Ciabattoni, Timo Lang, Revantha Ramanayake
2022-03-04
Logic in Computer Science · Computer Science
A cut-free sequent calculus for the bi-intuitionistic logic 2Int
Sara Ayhan
2020-10-01
Logic · Mathematics
A Constructive Proof of Cut Elimination for a System of Full Second Order Logic
Sandro Skansi
2016-06-22
Logic in Computer Science · Computer Science
Cut Elimination for a Logic with Induction and Co-induction
Alwen Tiu, Alberto Momigliano
2010-10-01
Logic in Computer Science · Computer Science
Cut Elimination in Multifocused Linear Logic
Taus Brock-Nannestad, Nicolas Guenot
2015-02-18
Logic in Computer Science · Computer Science
Cut-restriction: from cuts to analytic cuts
Agata Ciabattoni, Timo Lang, Revantha Ramanayake
2023-05-01
Logic in Computer Science · Computer Science
A new calculus for intuitionistic Strong L\"ob logic: strong termination and cut-elimination, formalised
Ian Shillito, Iris van der Giessen, Rajeev Goré, Rosalie Iemhoff
2023-09-04
Logic in Computer Science · Computer Science
A sequent calculus with procedure calls
Mahfuza Farooque, Stéphane Lengrand
2012-04-24
Logic in Computer Science · Computer Science
Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents
Akinori Maniwa, Ryo Kashima
2025-01-03
Logic in Computer Science · Computer Science
SLD-Resolution Reduction of Second-Order Horn Fragments -- technical report --
Sophie Tourret, Andrew Cropper
2019-02-27
Logic in Computer Science · Computer Science
The problem of Pi_2-cut-introduction
Alexander Leitsch, Michael Peter Lettmann
2018-01-16
Logic in Computer Science · Computer Science
A Labelled Sequent Calculus for Public Announcement Logic
Hao Wu, Hans van Ditmarsch, Jinsheng Chen
2022-10-28
Logic · Mathematics
Sequent Calculi for some subintuitionistic Logics
Fatemeh Shirmohammadzadeh Maleki
2024-10-29
Optimization and Control · Mathematics
Learning to Remove Cuts in Integer Linear Programming
Pol Puigdemont, Stratis Skoulakis, Grigorios Chrysos, Volkan Cevher
2024-06-28
Logic in Computer Science · Computer Science
A Deep Inference System for Differential Linear Logic
Matteo Acclavio, Giulio Guerrieri
2022-01-03
Logic · Mathematics
Residuated Basic Logic I
Minghui Ma, Zhe Lin
2014-03-14
Logic · Mathematics
Cut-eliminability in second order logic calculi
Toshiyasu Arai
2017-01-05
Logic in Computer Science · Computer Science
Cut-Simulation and Impredicativity
Christoph Benzmueller, Chad E. Brown, Michael Kohlhase
2019-03-14
Logic in Computer Science · Computer Science
A Sequent Calculus for Modelling Interferences
Christophe Fouqueré
2007-06-25
Logic in Computer Science · Computer Science
Proof search for propositional abstract separation logics via labelled sequents
Zhe Hou, Ranald Clouston, Rajeev Gore, Alwen Tiu
2013-11-27
Logic · Mathematics
Proof Theory for Intuitionistic Strong L\"ob Logic
Iris van der Giessen, Rosalie Iemhoff
2023-03-07
Logic in Computer Science · Computer Science
Generic Modal Cut Elimination Applied to Conditional Logics
Dirk Pattinson, Lutz Schröder
2015-07-01
Logic in Computer Science · Computer Science
Relating Sequent Calculi for Bi-intuitionistic Propositional Logic
Luís Pinto, Tarmo Uustalu
2011-01-31
Programming Languages · Computer Science
Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program Termination
Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori +2
2021-09-02
Logic in Computer Science · Computer Science
Extending a system in the calculus of structures with a self-dual quantifier
Luca Roversi
2014-06-09