# Proof of formulas in sequent calculus

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?

• Sequent calculus refers to a style of formal proofs in the full predicate calculus. It's unclear what you are asking for, algorithms to check proofs (easy), algorithms to discover proofs (hard), or something else. It would help your Readers to provide useful responses if you gave more context to this request. Jun 26, 2015 at 12:52
• @hardmath, algorithms to discover proofs Jun 30, 2015 at 17:28