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

*To*: pvs@csl.sri.com*Subject*: Re: Using PVS to help teach logic (fwd)*From*: Mark Lawford <lawford@mcmaster.ca>*Date*: Mon, 28 Sep 1998 18:28:02 -0400 (EDT)

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

- Prev by Date:
**Re: PVS Version 2.2 now available** - Next by Date:
**Re: Using PVS to help teach logic (fwd)** - Prev by thread:
**Re: remove** - Next by thread:
**Re: Using PVS to help teach logic (fwd)** - Index(es):