MathGroup Archive 1995

[Date Index] [Thread Index] [Author Index]

Search the Archive

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








  • Prev by Date: Re: histogram
  • Next by Date: Re: Weirdness in Encapsulated Postscript (Windows version)?
  • Previous by thread: Proof Generator using Rules of Inference
  • Next by thread: histogram