Re: Proof Generator using Rules of Inference

*To*: mathgroup at smc.vnet.net*Subject*: [mg2090] Re: Proof Generator using Rules of Inference*From*: kitchin at kitchin.ultranet.com (John Kitchin)*Date*: Fri, 29 Sep 1995 01:14:10 -0400*Organization*: UltraNet Communications, Inc.

>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. 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_Bauer at 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