Article View: sci.logic
Article #602Re: Looking for proof checking/building software for teaching
From: Hardy Hulley
Date: Mon, 23 Nov 1992 23:43
Date: Mon, 23 Nov 1992 23:43
27 lines
1550 bytes
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
Technical Details
Message-ID:
<1992Nov23.234310.28222@ucthpx.uct.ac.za>Path:
arc1-ca.pugleaf.net!sparky!uunet!zaphod.mps.ohio-state.edu!saimiri.primate.wisc.edu!usenet.coe.montana.edu!ogicse!psgrain!ee.und.ac.za!ucthpx!elc.mth.uct.ac.za!hardyReferences:
<45@beech.ukc.ac.uk>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!sparky!uunet!zaphod.mps.ohio-state.edu!saimiri.primate.wisc.edu!usenet.coe.montana.edu!ogicse!psgrain!ee.und.ac.za!ucthpx!elc.mth.uct.ac.za!hardy From: hardy@elc.mth.uct.ac.za (Hardy Hulley) Newsgroups: sci.logic Subject: Re: Looking for proof checking/building software for teaching Message-ID: <1992Nov23.234310.28222@ucthpx.uct.ac.za> Date: 23 Nov 92 23:43:10 GMT Article-I.D.: ucthpx.1992Nov23.234310.28222 References: <45@beech.ukc.ac.uk> Sender: news@ucthpx.uct.ac.za (UCT News Admin.) Organization: University of Cape Town Lines: 27 X-Newsreader: Tin 1.1 PL4