Re: [isabelle] How do I write the sequent |- P in Isar using theorem

On Sat, 29 Jun 2013, Gottfried Barrow wrote:

There's a 3 page section in isar-ref.pdf titled "The sequent caclulus", page 201, which I guess will help me eventually figure it out.

It says,

  For certain proofs in classical logic, it can not be called natural.
  The sequent calculus, a generalization of natural deduction, is
  easier to automate.

That is a slightly different thing: "Sequent calculus" is meant here in the classic sense, with multiple conclusions and rules that allow shifting between assumptions and conclusions in the classic dual fashion. (Don't show this to constructivists, they will find it unintuitive despite Wikipedia saying "other intuitive explanations are possible, which are classically equivalent".)

What Larry explains in that chapter is how to use Pure rules (with their !! / ==> structure and single conclusion) to represent the idea behind classical sequent calculus naturally. It all works out rather nicely in the end, leading to proof tools like "fast" and "best" that where a big thing in the early 1990-ies (with minimal implementation effort). A bit later came "blast", with the same rule representation, but different inferencing engine.

Nowadays people tend to appeal to more heavy gear: sledgehammer and metis for reconstruction, but that is quite different technology and unrelated to this thread.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.