[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?
[31 December 2010]

The view from Black Mesa is a new blog I have started, for posts related to digital preservation, data longevity, and the use of descriptive markup in institutions (especially but not limited to memory institutions: libraries, museums, archives).

Readers of this blog will find the style and many of the pre-occupations familiar, but the new blog will probably have fewer excursions into random topics not relevant to the mission of Black Mesa Technologies.