[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Using PVS to help teach logic (fwd)

Hello fellow PVS users.

I've had several requests to post a summary of the responses I received to
my earlier post on using PVS to teach logic so if you are interested,
please read on. 

At the moment it does not appear that there are any other users trying to
use PVS in an introductory logic course, though several people expressed
interest in hearing about my experiences with my 2nd year Applications of
Mathematical Logic for Software Engineering course.  I'll post a brief
report here towards the end of the term.

The one response I had from someone using PVS at the undergraduate level
was from Dr. Perry Alexander at The University of Cincinnati.  His
response is reposted below with his permission.  I'll follow this up with
in another post addressing some of the issues he raises.


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
Hamilton, Ontario  Canada L8S 4K1

---------- Forwarded message ----------
Date: 21 Sep 1998 09:55:29 -0400
From: Perry Alexander <alex@ececs.uc.edu>
To: Mark Lawford <lawford@mcmaster.ca>
Subject: Re: Using PVS to help teach logic (fwd)

Mark Lawford <lawford@mcmaster.ca> writes:

> Below is a copy of a message that I sent to the PVS mailing list asking if
> anyone had experience using PVS to teach introductory logic with
> applications to software engineering.  A graduate student from your
> department (Narendra Narasimhan) wrote back that you had been teaching a
> software engineering course using PVS for the past three years.  
> If you do not mind my enquiring, how have you found the experience of
> teaching logic with PVS as a tool?

I've never actually tried to teach beginning logic with PVS.  I teach
my students Z in their first course, so they enter the course that
uses PVS with some background in predicate calculus and natural
deduction proofs.  Using PVS in the specification and verification
course has been a fantastic experience.  The students love PVS and at
that level it really works nicely.

I have some thoughts on trying to teach a general logic course based
on what I've observed in our specification and verification course.

First, the negative aspects:

1. There are very few books that teach logic using a sequent calculus
proof style.  Offhand, Manna and Waldinger's book is the only one I
can think of.  Most books I know of use a natural deduction style.  (I
should qualify that with the fact that I pretty much only look at
formal methods books, not basic logic or discrete math texts.)  That's
a real problem.  It may not be a huge leap from natural deduction to
sequent calculus for someone with some background, it's a huge leap for
a beginner.  Maybe first year grad students could deal with it, but
undergraduates will struggle I think.

2. One pragmatic issue is PVS documentation.  What's there is is
pretty good, but it's getting very old.  Certainly not for beginners,
but that's not SRI's target audience.  Again, that might not be a
problem for typical users, but it is a problem for students.

3. Most beginning propositional logic proofs can be discharged with
flatten and split applied relatively mindlessly.  Predicate calculus
proofs are not much harder once skolemization is introduced.  In my
second course, I have the students re-prove their first 4 homework
assignments from the first course using PVS.  They completely freak
until they try it.  What took them weeks by hand takes them about an
hour using PVS.  Most of that involves typing the theories in.

4. The worst aspect pedagogically is that PVS gives the student little
or no insight into how the proof is proceeding.  To begin with,
sequent calculus obfuscates things for most students.  Then, PVS
charges ahead and makes that worse.  Even with PVS I really don't
think it's possible for a student to automate a reasonably sized proof
that they can't do by hand.  So, understanding how the proof unfolds
is, to me, critical.

Now the positive aspects:

1. Students who would never dream of completing a proof by hand will
destroy themselves trying to get PVS to do it.  Effectively, proving
becomes programming and many students really respond to that.  The
same mentality that drives them to complete a program drives them to
complete the proof.

2. PVS provides immediate feedback.  The students know quickly whether
their proof is correct or not, thus contributing to point 1.  This is
incredibly powerful.  Students learn to hack the theorem prover and
that eventually leads to deeper understanding.

3. Once you get to computer science/engineering subjects, the students
have something that they can really work with.  PVS really wasn't
designed for teaching basic logic, but it's extremely well designed
for specification and verification.  Once you get to that point in
your curriculum, the students will be able to do some wonderful
things.  As I mentioned earlier, my experience has been great.

In all honesty, I think all of my problems could be addressed with an
appropriately designed course and text.  I've thought about writing a
junior level software engineering text that uses PVS.  Time is always
a problem and designing the layout and information flow is really
hard.  Heck, just a web page wears me out!  Maybe after a few more
years experience...

Please let me know how things turn out or if there's any way I can
help.  I work with a DARPA Consortium on formal methods education.
There are several folks involved (including me) who would love to help
out in any way we can.

- Perry

     Dr. Perry Alexander / ECECS Dept. / The University of Cincinnati
       PO Box 210030 / 896 Rhodes Hall / Cincinnati, OH 45221-0030
               513.556.4762 (Voice) / 513.556.7326 (FAX)
         perry.alexander@uc.edu / http://www.ececs.uc.edu/~alex