[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:44:35 -0400 (EDT)*Cc*: Perry Alexander <alex@ececs.uc.edu>

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 Hamilton, Ontario Canada L8S 4K1 ---------- 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 your reply), we are using the textbook "Mathematical Logic: Applications 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. Thanks again Perry. You've already been most helpful through your web pages and your detailed e-mail response. Regards, Mark

- Prev by Date:
**Re: Using PVS to help teach logic (fwd)** - Next by Date:
**PVS Batch Mode** - Prev by thread:
**Re: Using PVS to help teach logic (fwd)** - Next by thread:
**PVS Batch Mode** - Index(es):