From: Ted Knupke <tknupke@mitre.org>
Subject: Re: where can I find a predicate calculus editor/theorem checker?
Date: Mon, 20 Sep 1999 16:44:40 -0400
Newsgroups: sci.math,sci.math.symbolic

Paul Elliott wrote:

> Is anyone aware of a predicate calculus editor/theorem checker?
>
> I was hoping for some software that would allow you to point and
> click at previous assertions or axioms, and have it write out
> the next assertion via the inference rule or substitution indicated.
>
> Does such a thing exist?
>
> Paul Elliott                          Telephone: 1(512)837-9345
> pelliott@io.com                       Address:   PMB 181, 11900 Metric Blvd Suite J
> http://www.io.com/~pelliott/pme/      Austin TX 78758-3117

There are a number of theorem provers around that will do predicate
calculus.   This has been on my own list of "things to look into" for a
while, but I have not had time to do anything.   You might want to
check out some of the links at

http://www-formal.stanford.edu/clt/ARS/systems.html

Ted