Proof of formulas in sequent calculus

Question

Is there an algorithm for proof of formulas in sequent calculus, like resolution method? I'm especially interested in natural deduction.

UPDATE

Well, we have one scheme of axioms $$\Phi\vdash\Phi$$ and twelve rules of inference: $$ \begin{align} 1.\enspace&\frac{\Gamma\vdash\Phi;\Gamma\vdash\Psi}{\Gamma\vdash\Phi\wedge\Psi} & 7.\enspace&\frac{\Gamma,\Phi\vdash\Psi}{\Gamma\vdash\Phi\to\Psi}\\\\ 2.\enspace&\frac{\Gamma\vdash\Phi\vee\Psi}{\Gamma\vdash\Phi} & 8.\enspace&\frac{\Gamma\vdash\Phi;\Gamma\vdash\Phi\to\Psi}{\Gamma\vdash\Psi}\\\\ 3.\enspace&\frac{\Gamma\vdash\Phi\vee\Psi}{\Gamma\vdash\Psi} & 9.\enspace&\frac{\Gamma,\neg\Phi\vdash}{\Gamma\vdash\Phi}\\\\ 4.\enspace& \frac{\Gamma\vdash\Phi}{\Gamma\vdash\Phi\vee\Psi} & 10.\enspace&\frac{\Gamma\vdash\Phi;\Gamma\vdash\neg\Phi}{\Gamma\vdash}\\\\ 5.\enspace&\frac{\Gamma\vdash\Psi}{\Gamma\vdash\Phi\vee\Psi} & 11.\enspace&\frac{\Gamma,\Phi,\Psi,\Gamma_1\vdash X}{\Gamma,\Psi,\Phi,\Gamma_1\vdash X}\\\\ 6.\enspace&\frac{\Gamma,\Phi\vdash \Psi; \Gamma, X\vdash \Psi; \Gamma\vdash\Phi\vee X}{\Gamma\vdash\Psi} & 12.\enspace&\frac{\Gamma\vdash\Phi}{\Gamma, \Psi\vdash\Phi} \end{align} $$

Is there an algorithm for proof of formulas in this calculus?

Answer 1

There is no such thing as the sequent calculus (even for a particular logic, like -- to keep things simple -- classical propositional logic). There is a number of varieties.

There is no such thing as the natural deduction calculus (for the same logic) either.

But on any story, sequent calculi and natural deduction systems are different sorts of beasts (though there are versions of the sequent calculus which are said to be "natural deduction style", but they aren't natural deduction calculi).

This means that the question really isn't very well posed at it stands. Perhaps you'd like to sharpen it up?

I'll add that if you want a clear modern introduction to sequent calculus and their relation to natural deduction, the place to go is Sara Negri and Jan von Plato's Structural Proof Theory. They also talk about proof search methods for various calculi.