I'm afraid my earlier request for a proof checker was not sufficiently
clear. What I was really looking for was an interactive proof
editor/verifier. In particular, I am NOT looking for a logical
inference engine (such inference engines are quite easy to find).
I HAVE the inferences, but I would like to make sure I've derived them
properly. For this an inference engine is not at all what I need. I
need a program which allows me to say something like "now I apply the
rule of universal instantiation to step 5, for the universally
quantified variable $x$." Inference engines don't provide this
facility. And, for that matter, you don't need an inference engine to
get this facility --- most of the allowable proof actions are fairly
rudimentary syntactic transformations.
Strange as it may seem, I DID look at the FAQs for Lisp and Prolog.
There were many inference engines but only 1 proof checker: pc, which
is built on top of the Boyer-Moore theorem prover. This program seems
to have both much more than I need (ability to prove theorems by
itself) and much less (a fairly nasty user interface). So please, I
appreciate the thought, but no more pointers to those files!
Any other advice would be very much appreciated,
Thanks,
r
In article <··················@palette.src.honeywell.com> ·······@src.honeywell.com (Robert P. Goldman) writes:
I'm afraid my earlier request for a proof checker was not sufficiently
clear. What I was really looking for was an interactive proof
editor/verifier. In particular, I am NOT looking for a logical
inference engine (such inference engines are quite easy to find).
I HAVE the inferences, but I would like to make sure I've derived them
properly. For this an inference engine is not at all what I need. I
need a program which allows me to say something like "now I apply the
rule of universal instantiation to step 5, for the universally
quantified variable $x$." Inference engines don't provide this
facility. And, for that matter, you don't need an inference engine to
get this facility --- most of the allowable proof actions are fairly
rudimentary syntactic transformations.
Strange as it may seem, I DID look at the FAQs for Lisp and Prolog.
There were many inference engines but only 1 proof checker: pc, which
is built on top of the Boyer-Moore theorem prover. This program seems
to have both much more than I need (ability to prove theorems by
itself) and much less (a fairly nasty user interface). So please, I
appreciate the thought, but no more pointers to those files!
This is a very reasonable idea, indeed there is a European research
programme which precisely covers this topic: "Basic Research Action on
Types for Proofs and Programs". During this and the preeceding BRA a
number of proof-checker, editor, libraries and proofs have been
developed. Just to give a few examples of systems:
Coq INRIA/Roquencourt, Paris
LEGO Edinburgh University
ALF Chalmers University, Gothenburg
ISABELLE Cambridge University
All these systems are in some way based on typed lambda calculi and
Type Theory. Outside the BRA there are:
NuPRL Cornell University
ELF Carnegie Mellon University
and many more which don't come to mind in the moment or which I don't
know.
Given the amount of work being done it is may be a bit surprising that
there is no newsgroup and therefore no FAQ for this topic. Maybe one
should change this.
However, there is a moderated mailing list about Type Theory
(·············@dcs.gla.ac.uk). Most of the systems I mentioned above
are available by ftp - all are to some degree experimental (try archie
or mail me when you get stuck). The proceedings of the BRA workshops
have been partially published in Oxford University Press, the latest
(informal) proceedings are available by annonymous ftp from
ftp.cs.kun.nl (/pub/csi/CompMath/Types/NijmegenTypes.{ps,dvi}.Z).
Soem of the stuff in there is quite technical.
--
Thorsten Altenkirch Host: muppet77.cs.chalmers.se Office: 2438
snail: Dep. of Computer Science; Chalmers U. of Technology; 412 96 Gothenburg
phone: (+ 46 31) 772 1079 [office], (+ 46 31) 40 24 72 [home] Sweden
From: SR. Ferguson
Subject: Re: more on request for proof checker
Date:
Message-ID: <CGDMK3.5nx@info.bris.ac.uk>
Robert P. Goldman (·······@src.honeywell.com) wrote:
: I'm afraid my earlier request for a proof checker was not sufficiently
: clear. What I was really looking for was an interactive proof
: editor/verifier. In particular, I am NOT looking for a logical
: inference engine (such inference engines are quite easy to find).
: I HAVE the inferences, but I would like to make sure I've derived them
: properly. For this an inference engine is not at all what I need. I
: need a program which allows me to say something like "now I apply the
: rule of universal instantiation to step 5, for the universally
: quantified variable $x$." Inference engines don't provide this
: facility. And, for that matter, you don't need an inference engine to
: get this facility --- most of the allowable proof actions are fairly
: rudimentary syntactic transformations.
: Strange as it may seem, I DID look at the FAQs for Lisp and Prolog.
: There were many inference engines but only 1 proof checker: pc, which
: is built on top of the Boyer-Moore theorem prover. This program seems
: to have both much more than I need (ability to prove theorems by
: itself) and much less (a fairly nasty user interface). So please, I
: appreciate the thought, but no more pointers to those files!
: Any other advice would be very much appreciated,
: Thanks,
: r
Dear Robert,
I know of a package, called MacLogic, which has two modes, construct and
check; construct allows you to do Gentzen/Lemmon style proofs, as well as
do tactical derivations, similar to Gentzens LK, LJ, LM, etc.
It was written in St. Andrews, Scotland, where the cs department do loads
of work on this sort of thing. The package MacLogic was used as part of
the Machine Assisted Logic Teaching Programme, teaching logic to first and
second year philosophy students.
For a copy, you could contact its creater, Ron Dyckhoff; his e-mail
address is: ··@cs.st-and.ac.uk
I do not know if this package is available generally or not, but write
him, and see what he says.
Yours sincerely,
Stephen