Proof Generator using Rules of Inference

[Orlando Furlan]

Hello !
I would like to know if exist some package or notebook for
proof a conclusion from a set of premises, using rules of inference
something like a "Proof Generator". Or some specific from Propositional
Calculus.
Thanks for this help in advance. Greetings from Nicaragua
earth from lakes and volcanos.

Orlando Furlan
National University of Engineering
Managua, Nicaragua.

[John Kitchin]

Greetings from Massachussetts, earth (with lots of rocks) from Northern Canada
(a gift from the last Ice Age)

Analytica is an automatic theorem prover written in Mathematica 1.1, developed
by Edmund Clarke and others at Carnegie Mellon University. In March of this
year it was available via anonymous ftp from "gs204.sp.cs.cmu.edu" in directory
/pub/analytica.

Andrej...@PARALLEL.SCANDAL.CS.CMU.EDU was very helpful to me
in getting started with it.

The ftp available version runs under UNIX. With minor alterations (filename
changes). I got Analytica to run under Windows 3.1 and Mathematica 2.0.

My interest is in proving conjectures in Mathematical Statistics. Analytica
looks like a good starting point, though it will need to be taught a lot of
additional rules.

Good Luck. I'd be interested in hearing about your work (by email).
/John K