dc.contributor.author Allen, Stuart en_US dc.contributor.author Constable, Robert en_US dc.contributor.author Fluet, Matthew en_US dc.date.accessioned 2007-04-04T19:34:38Z dc.date.available 2007-04-04T19:34:38Z dc.date.issued 2004-03-26 en_US dc.identifier.citation http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2004-1933 en_US dc.identifier.uri https://hdl.handle.net/1813/5644 dc.description.abstract In Smullyan's classic book, First-Order Logic, the notion of a Boolean valuation is central in motivating his analytical tableau proof system. Smullyan shows that these valuations are unique if they exist, and then he sketches an existence proof. In addition he suggests a possible computational procedure for finding a Boolean valuation, but it is not related to to the existence proof. A computer scientist would like to see the obvious explicit recursive algorithm for evaluating propositional formulas and a demonstration that the algorithm has the properties of a Boolean valuation. Ideally, the algorithm would be derived from the existence proof. It turns out to be unexpectedly difficult to find a natural existence proof from which the algorithm can be extracted, and it turns out that the implicit computational content of Smullyan's argument is not found where one might expect it. We show that using the notion of a very dependent function type, it is possible to specify the Boolean valuation and prove its existence constructively so that the natural recursive algorithm is extracted and is known to have the mathematically required properties by virtue of its construction. We illustrate all of these points using the Nuprl proof development system. en_US dc.format.extent 203471 bytes dc.format.mimetype application/pdf dc.language.iso en_US en_US dc.publisher Cornell University en_US dc.subject computer science en_US dc.subject technical report en_US dc.title Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations en_US dc.type technical report en_US
﻿