E1AR0002@SMUVM1.BITNET.UUCP (03/25/87)
Past Seminar, Southern Methodist University, Department of Computer Science
Natural Deduction meets Schubert's Steamroller
Frank Vlach
Texas Instruments
Schubert's Steamroller is a test problem for automatic theorem provers
that has attracted a lot of attention recently, and has proved
difficult for resolution theorem provers. A human theorem prover
would prove Schubert's Steamroller using a `natural' but mechanical
and totally non-creative method that is readily programmable and quite
different from resolution. Hand computations indicate that this
strategy is much less complex than resolution for Schubert's
Steamroller and a number of similar problems. An implementation is in
progress in order to compare this method with resolution (and other
methods) over a wide range of problems.
This strategy also has the advantage that it requires no preprocessing
of formulas (such as Skolemization or conversion to clausal form), and
lends itself to the generation of natural proofs, readable by humans.