# Questions tagged [sequent-calculus]

For questions concerning sequent calculus, a formal proof system originally introduced by Gerhard Gentzen in 1933/1935 and studied in the framework of proof theory.

194 questions
Filter by
Sorted by
Tagged with
1 vote
56 views

### Examples of sequent derivations that uses cut rule that can be modified to not to use cut rule?

The cut-elimination theorem states that any sequent calculus derivation that uses the cut rule also has a derivation that does not use the cut rule. I cannot find any explicit examples of such ...
• 525
75 views

### Deriving $\Phi\vdash\Delta$ from $\lnot\lnot\Phi\vdash\Delta$ without cut rule?

I revisited the old post of mine and I am confused with the answer. The cut elimination theorem states that for any sequent that is derived with cut rule, there exists a derivation of the same sequent ...
• 525
72 views

### Use sequent calculus to show if $\Gamma\vdash t_1=t_2$ then $\Gamma\vdash f(t_1)=f(t_2)$

Suppose the sequent $\Gamma\vdash t_1=t_2$ where $t_1,t_2$ are closed terms. Let $f$ be a one-place function symbol. I am trying to find a sequent calculus derivation of $\Gamma\vdash f(t_1)=f(t_2)$ ...
• 525
1 vote
31 views

• 328
1 vote
93 views

### Is there a G4ip equivalent for first-order logic?

G4ip is a sequent calculus for propositional logic (by Dyckhoff) that is contraction-free, thus (if I understand correctly) greatly simplifying the writing of automated theorem provers by avoiding ...
• 13
62 views

• 783
1 vote
378 views

### Natural Deduction Proof search algorithm for Classical Propositional logic?

I know of two algorithms for determining classical propositional validity: Convert the problem into a SAT problem, run a SAT solver. These algorithms are efficient, but it seems difficult/infeasible ...
• 151
1 vote
161 views

### "forward" natural deduction vs "backward" natural deduction

Updated Question I'm following Interactive Tutorial of the Sequent Calculus which states the rules for "backwards" deduction and comparing it to the rules for "forward" natural ...
• 1,477
1 vote
84 views

### Natural Deduction and Sequent Calculus

Are there any good natural deduction and sequent calculus solvers online for both predicate and propositional logic? Or perhaps forums that specialise in these proof systems?