# Re: Using PVS to help teach logic (fwd)

```
Hello again.

Here are some excerpts from my response to Perry's comments.

The online tutorial for the sequent calculus mentioned below can be found
through Perry's homepage at

http://www.ececs.uc.edu/~alex/

with a little hunting, or more directly at:

http://www.ececs.uc.edu/~alex/teach/ece793/sequent.html

Mark

Dr. Mark Lawford
Assistant Professor                        Email: lawford@McMaster.ca
DEPARTMENT OF COMPUTING AND SOFTWARE       Tel: 905 525 9140 Ext. 24911
Faculty of Engineering                     Fax: 905 525 6246
McMaster University,                       Office: JHE 302/C

---------- Forwarded message ----------
Date: Wed, 23 Sep 1998 18:32:25 -0400 (EDT)
From: Mark Lawford <lawford@mcmaster.ca>
To: Perry Alexander <alex@ececs.uc.edu>
Subject: Re: Using PVS to help teach logic (fwd)

Hi Perry.

Thanks the reply and the offer of help.  There are two ways in which you
can help right away.  First, I'd like to be able to repost your reply to
the PVS mailing list as a part of my summary of responses to my original
post.  Second, I'd like to use your online Sequent Calculus as a class
handout (with appropriate credit of course) or at least be able to refer
my students to the online tutorial.

In my course, which is currently underway (hence the delayed response to
and Theory" by Jean E. Rubin. It uses the natural deduction style for
teaching logic and is rather thin on the applications, though it is quite
readable.  After covering predicate logic over the next 2-3 weeks, we'll
set it aside until we return to proof by induction.  Next Wednesday I'll
show them how PVS can be used to perform propositional reasoning, then
predicate logic a few weeks later.  PVS should play a major role when I
talk about types and type checking in the weeks following predicate logic.

Your tutorial on the sequent calculus could help the students make the
transition from natural deduction to sequent calculus.  Regarding your
concerns about the sequent calculus obscuring proof structure, I've found
the "x-show-proof" and "x-step-proof" commands very helpful in this
regard, especially for the types of small problems the students will be
dealing with.  We'll see how the students make the transition from natural
deduction to sequent calculus, but I think that knowing both will serve
them well and the differences may be transparent in many ways.  For
instance, the way that PVS deals with implications in the consequent can
also be viewed as an instance of the Deduction Theorem at work.