Thread View: sci.math.symbolic
2 messages
2 total messages
Started by Anthony J.R. Heading
Tue, 26 Jan 1993 16:49
Automatic Theorem Proving?
Author: Anthony J.R. Heading
Date: Tue, 26 Jan 1993 16:49
Date: Tue, 26 Jan 1993 16:49
17 lines
1151 bytes
1151 bytes
I want to write a computer algebra/theorem proving system, basically as a learning exercise and a testbed for any new ideas I might have. I guess, though, that this has been done a million times in the past, so I want to find out about important existing systems. I've done a literature search which has revealed singularly little, so the next approach is to ask the people on the ground...I don't want to buy any of the commercial packages - I'm interested in finding out about the underlying principles. Can anyone refer me to articles, papers, or even software, from which I can infer the current wisdom? Also, are there any meetings or conferences which discuss this sort of thing? Thanks Anthony Heading
Re: Automatic Theorem Proving?
Author: U54294
Date: Thu, 28 Jan 1993 00:55
Date: Thu, 28 Jan 1993 00:55
30 lines
2187 bytes
2187 bytes
In article <1k3q28INN82l@signal.dra.hmg.gb>, heading@ccint1.rsre.mod.uk (Anthony J.R. Heading) says: > >I want to write a computer algebra/theorem proving system, basically >as a learning exercise and a testbed for any new ideas I might have. >I guess, though, that this has been done a million times in the past, >so I want to find out about important existing systems. > >Thanks >Anthony Heading > The title "Automated Reasoning" by Ewing, Overbeek, Lusk, Boyle (did I forget anyone?) just came out in an expanded second edition. It includes a diskette containing the Otter 2.2 theorem proving system. The text is something of a tutorial, but you can easily skip to the more "formal" chapters if you prefer. There is also a reference chapter on Otter and a chapter on Prolog as a theorem proving system. The disk contains source, documentation and executables for DOS. Other versions are available for Unix. I believe that the publisher is Prentice-Hall. All the authors are at Argonne National Labs here in the beautiful Chicago area. You can contact otter@mcs.anl.gov for further information on Otter. If you can't locate the book, get ahold of me and I'll provide a fuller citation. The tome's at home. +----------------------------------+------------------------------------+ | | I have noted in a Manchester | | Nick Geovanis | newspaper that I have proved might | | U54294@uicvm.uic.edu <--BEST | is right and therefore that every | | GEONI02@hera.cai.com | cheating tradesman is also right. | | | -- Darwin to Lyell, 1860 | +-----------------------------------------------------------------------+
Thread Navigation
This is a paginated view of messages in the thread with full content displayed inline.
Messages are displayed in chronological order, with the original post highlighted in green.
Use pagination controls to navigate through all messages in large threads.
Back to All Threads