Portal de Periódicos da CAPES

Software Review: The Great Theorem Prover Newborn Software 4874 Westmount St. Westmount, Quebec, Canada H3Y 1Y1; $30.00

1991; Association for Computing Machinery; Volume: 2; Issue: 4 Linguagem: Inglês

10.1145/122344.1063895

2331-1673

Don Cohen,

Logic, programming, and type systems

This product --- I'll refer to it as TGTP --- is a resolution theorem prover that runs on a standard IBM PC (not requiring anything like a 286, lots of memory, graphics, etc.). It contains several programs, some sample files and a manual of a little over 100 pages. It not only describes how to use the programs but also attempts to teach the reader how they work, and in the process, something about logic and resolution theorem provers in general. The preface says that, in addition to actually proving theorems, TGTP can be used for teaching theorem proving techniques. It is claimed to be understandable by high school students with a good mathematical background. I am not in a position to agree or disagree with this claim, but I have my doubts. It is also supposed to be of interest to mathematicians curious about progress in mechanical theorem proving, college students studying the subject and specialists in the area. TGTP evidently started out as a teaching aid for an AI course. For specialists I don't expect that it will be of more than passing interest, although it also has some entertainment value.