Questions tagged [sequent-calculus]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
10
votes
1answer
184 views

Typo in the calculus of constructions paper?

In the classic the calculus of constructions paper there is a rule that states (page 7 of the pdf, page 101 of the original document) This rule would mean that any context is reducible to a member ...
4
votes
1answer
106 views

Sequent calculus for nonmonotonic/defeasible logics?

Is it possible to construct sequent calculus for nonmonotonic/defeasible logic? If it is possible then those logics can be encoded in proof assistants which require sequent calculus for logic to be ...
3
votes
0answers
95 views

How to develop an effective notation for a partially ordered logic?

I am developing a logic for reasoning about programs in a resource-constrained environment. My starting point is intuitionistic linear logic, but I made the following changes: In intuitionistic ...
3
votes
2answers
378 views

Derivation of cut rule in sequent calculus

I searched internet but could not find any good weblink which shows how the cut rule for sequent calculus can be derived. I found this paper but it uses implication elimination rule which I cannot ...
10
votes
1answer
238 views

Unification-based elimination rule for equality

A few years back, I ran across the following left-rule for equality in sequent calculus: $$ \frac{s \doteq t \leadsto \theta \qquad \theta(\Gamma) \vdash \theta(C)} {\Gamma, s \doteq t ...
6
votes
1answer
168 views

converse relationship between the cut rule and the identity axiom

On page 30 of "Proofs and Types" by Girard, Taylor, and Lafont, it is claimed that that the identity axiom for sequent calculus: C ├ C has a converse relation with the cut rule: $$\frac{\vec{A} \...
14
votes
2answers
269 views

Cut-elimination for calculus with nats or other inductive datatype?

Does anyone direct me to a paper detailing a cut-elimination theorem for propositional intuitionistic logic, including an inductive datatype such as the natural numbers (lists or trees would be fine, ...
8
votes
2answers
380 views

About the correspondence of left introduction and elimination of implication in Sequent Calculus and in Natural Deduction resp.

Could anyone give an intuitive (not intutionistic) explanation of the correspondence of left introduction and elimination of implication in Sequent Calculus (SC) and Natural Deduction (ND) ...