0
$\begingroup$

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?

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – hardmath
    Jun 26, 2015 at 12:52
  • 1
    $\begingroup$ @hardmath, algorithms to discover proofs $\endgroup$ Jun 30, 2015 at 17:28

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
0

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .