A sequent calculus with procedure calls
Mahfuza Farooque (LIX, INRIA Saclay - Ile de France), St\'ephane, Lengrand (LIX, INRIA Saclay - Ile de France)
TL;DR
This paper introduces an extension of the sequent calculus LKF, called LK(T), which incorporates procedure calls and maintains cut-elimination, enhancing the calculus's capabilities for automated reasoning.
Contribution
The paper presents a novel extension of the sequent calculus with procedure calls and proves its cut-elimination property.
Findings
LK(T) extends LKF with procedure calls
Cut-elimination is proven for LK(T)
Enhances automated reasoning capabilities
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).
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge