A sequent calculus with procedure calls

2012/04/23 by Mahfuza Farooque, Farooque, Mahfuza, Stéphane Lengrand +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1204.5156

openalex publication_date 2012/04/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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).

Citations

• Solving SAT and SAT Modulo Theories

Related

• Sequent Calculi with procedure calls
• The Cut Elimination and the Nonlengthening Property for the Sequent Calculus with Equality
• The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)
• A theory of cut-restriction: first steps
• Contraction Elimination in Sequent Based Ground Equational Calculus