A sequent calculus with procedure calls
Logic in Computer Science
2012-04-24 v1
Abstract
In this paper, we extend the sequent calculus LKF into a calculus LK(T), allowing calls to a decision procedure. We prove cut-elimination of LK(T).
Keywords
Cite
@article{arxiv.1204.5156,
title = {A sequent calculus with procedure calls},
author = {Mahfuza Farooque and Stéphane Lengrand},
journal= {arXiv preprint arXiv:1204.5156},
year = {2012}
}
Related papers
View all related →
Logic in Computer Science · Computer Science
Sequent Calculi with procedure calls
Mahfuza Farooque, Stéphane Graham-Lengrand
2013-09-18
Logic in Computer Science · Computer Science
A Sequent Calculus for Modelling Interferences
Christophe Fouqueré
2007-06-25
Logic in Computer Science · Computer Science
A Sequent Calculus Proof Search Procedure and Counter-model Generation based on Natural Deduction Bounds
Jefferson de Barros Santos, Bruno Lopes Vieira, Edward Hermann Haeusler
2020-02-04
Logic in Computer Science · Computer Science
Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)
Rajeev Goré, Björn Lellmann
2019-07-03
Logic in Computer Science · Computer Science
Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic
Rajeev Gore, Linda Postniece, Alwen Tiu
2010-06-30
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
Fast Cut-Elimination using Proof Terms: An Empirical Study
Gabriel Ebner
2018-10-18
Logic · Mathematics
Parametric mixed sequent calculus
Karim Nour, Olivier Laurent
2009-05-12
Logic in Computer Science · Computer Science
A Sequent Calculus and a Theorem Prover for Standard Conditional Logics
Nicola Olivetti, Gian Luca Pozzato, Camilla Schwind
2007-05-23
Logic · Mathematics
Sequent Calculi for some subintuitionistic Logics
Fatemeh Shirmohammadzadeh Maleki
2024-10-29
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
Induction and Co-induction in Sequent Calculus
Alwen Tiu, Alberto Momigliano
2009-09-30
Logic · Mathematics
On structural proof theory of the modal logic K+ extended with infinitary derivations
Daniyar Shamkanov
2024-11-25
Logic in Computer Science · Computer Science
A Labelled Sequent Calculus for Public Announcement Logic
Hao Wu, Hans van Ditmarsch, Jinsheng Chen
2022-10-28
Programming Languages · Computer Science
Grokking the Sequent Calculus (Functional Pearl)
David Binder, Marco Tzschentke, Marius Müller, Klaus Ostermann
2025-04-29
Logic · Mathematics
Integrating a Global Induction Mechanism into a Sequent Calculus
David M. Cerna, Michael Peter Lettmann
2022-07-21
Logic · Mathematics
Cut elimination and normalization for generalized single and multi-conclusion sequent and natural deduction calculi
Richard Zach
2021-11-08
Logic in Computer Science · Computer Science
Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic
Bahareh Afshari, Johannes Kloibhofer
2025-11-05
Logic in Computer Science · Computer Science
The Functional Machine Calculus III: Choice (Early Announcement)
Willem Heijltjes
2024-11-08
Logic · Mathematics
Rule-Elimination Theorems
Sayantan Roy
2024-10-08
Category Theory · Mathematics
A language for multiplicative-additive linear logic
J. R. B. Cockett, C. A. Pastro
2010-03-03
Logic · Mathematics
Unsound Inferences Make Proofs Shorter
Juan P. Aguilera, Matthias Baaz
2019-05-07
Logic in Computer Science · Computer Science
Classical Transitions
Fabrizio Montesi, Marco Peressotti
2018-03-06
Logic in Computer Science · Computer Science
A Set-Theoretic Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted Quantifiers
Maximiliano Cristiá, Gianfranco Rossi
2022-08-09
Logic in Computer Science · Computer Science
The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them
Ekaterina Komendantskaya, Dmitry Rozplokhas, Henning Basold
2020-08-11