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.
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
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
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