[13 December 2010]
When I took an introductory course in symbolic logic, all those many years ago, we used a textbook (Richard C. Jeffrey, Formal logic: its scope and limits [New York: McGraw-Hill, 1967], in case you’re curious) which presented a proof method based on proof trees, which had the nice property that for valid inferences it’s guaranteed to terminate, and that for invalid inferences it will never terminate with a false positive. Allen Renear informs me that the locus classicus for proof trees is Raymond M. Smullyan, First-order logic (2d ed. New York: Dover, 1995), which I have been reading lately with pleasure.
All the theorem provers I’ve read about, however, seem to require more or less active participation and guidance from the user; like the proof-tree method, they produce a proof only when a proof exists, but unlike the proof-tree method they aren’t guaranteed to find a proof if one exists.
So I’ve been wondering: why aren’t there automatic theorem provers based on the proof-tree method?
Or are there?