Looking for proof checking/building software for teaching

Thread View: sci.logic

2 messages

[T] Back to Threads [V] Tree View [G] Group Articles

2 total messages Started by S.J.Thompson Mon, 23 Nov 1992 20:06

#598

Author: S.J.Thompson
Date: Mon, 23 Nov 1992 20:06

19 lines
1071 bytes

I am looking for software to support teaching propositional and predicate
logic at undergraduate level. Specifically, I would like software for the
IBM PC or for Sun workstations which support the interactive construction of
proofs. I will post a summary of responses, assuming I receive any, to the
net.

Many thanks

Simon Thompson

=======================================================================

Simon Thompson				e-mail:	sjt@ukc.ac.uk
Computing Laboratory			phone:	+44-227-764000 
University of Kent				  extn. 3820
Canterbury, Kent,			fax:	+44-227-762811
CT2 7NF, UK

=======================================================================

Re: Looking for proof checking/building software for teaching

#602

Author: Hardy Hulley
Date: Mon, 23 Nov 1992 23:43

27 lines
1550 bytes

sjt@ukc.ac.uk (S.J.Thompson) writes:
: I am looking for software to support teaching propositional and predicate
: logic at undergraduate level. Specifically, I would like software for the
: IBM PC or for Sun workstations which support the interactive construction of
: proofs. I will post a summary of responses, assuming I receive any, to the
: net.
: 
: Many thanks
: 
: Simon Thompson
 
Last year we wrote a very simple Predicate Calculus proof-checker which runs
on top of Cambridge University's HOL theorem prover. We had exactly the same
idea as you have - we got undergraduate students to construct their proofs
in the system, and the proof-checker then checked the validity of these proofs.

The HOL software runs beautifully on a Sun workstation, and writing a system
especially for Predicate Calculus is a simple exercise.

Hardy Hulley

Lab. for Formal Aspects and Complexity in Computer Science
University of Cape Town

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads