Proof Checker

Article View: sci.logic

Article #23

#23

From: Andrew Malton
Date: Thu, 29 Oct 1992 22:08

16 lines
1195 bytes

Anyone know where I can find a cheap and reliable proof checker for 
natural deduction derivations of the first-order predicate calculus?
Objective: teaching logic at the Second Year level. I'm hoping that the
proof language will be one that lends itself to proof theory, e.g., to the
translation to sequent calculus. (For this reason I prefer not to use a
system like MIZAR [Trybulec & al] whose language simulates ordinary
mathematical discourse.) I also don't want a system designed as a theorem
prover: just a checker!

Thanks for any help,
A Malton
-- 
Prof. Andrew Malton                  | Office (613) 545 6526
Dept. of Computing and Info. Science | FAX    (613) 545 6513
Queen's University                   | malton@qucis.queensu.ca
Kingston, Ontario, Canada K7L 3N6    |

Technical Details

Message-ID: <1992Oct29.220829.8091@qucis.queensu.ca>

Path: arc1-ca.pugleaf.net!sparky!uunet!utcsri!torn!news.ccs.queensu.ca!qucis.queensu.ca!malton

References: <24780@optima.cs.arizona.edu>

Show Full Headers

Complete Article Headers

Newsgroups: sci.logic
Path: arc1-ca.pugleaf.net!sparky!uunet!utcsri!torn!news.ccs.queensu.ca!qucis.queensu.ca!malton
From: malton@qucis.queensu.ca (Andrew Malton)
Subject: Proof Checker
Message-ID: <1992Oct29.220829.8091@qucis.queensu.ca>
Organization: Computing & Information Science, Queen's University at Kingston
References: <24780@optima.cs.arizona.edu>
Date: Thu, 29 Oct 1992 22:08:29 GMT
Lines: 16

Reply to Parent Message