I've been following, from a distance, Raph Levien's diary entries on theorem provers and mathematical logic in general. This would be greatly facilitated by Advogato's generating RSS feeds. Perhaps it's time to knuckle down and learn Stapler well enough to create my own feed.
In any event, I wonder whether Raph has looked at OBJ3 in the course of his investigations. The relevant paragraph from the description would seem to be this:
OBJ3 is based on order sorted equational logic, and has been successfully used for research and teaching in software design and specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among other things. It was the first language to implement parameterized programming and its module system influenced the designs of the Ada, C++ and ML module systems.
I hasten to point out that I have not used OBJ3 myself—although it's motivating me to install OpenMCL and see if OBJ3 will port easily. Joe Kiniry is an acquaintance, however, and I respect his work tremendously. Since Joe felt OBJ3 was important enough to maintain, I feel it's worth investigating further.
I'd also like to refer interested parties to OSCAR, but be warned: OSCAR's algorithms are patent-entangled. The foundational material for OSCAR can be found in Pollock's Cognitive Carpentry: A Blueprint for How to Build a Person, which I highly recommend. Given OSCAR's focus on being an architecture for a comprehensive theory of rationality, its applicability to theorem proving might not be obvious. However, OSCAR does subsume a complete deductive reasoner, and in competition based on the Thousands of Problems for Theorem Provers, OSCAR outperformed the highly-regarded Otter system both in number of problems successfully solved and by an astonishing performance measure with an average of 40 to 1, despite OSCAR's being written in fairly naïve Common Lisp vs. Otter's being written in C. I have to wonder if it wouldn't be possible to reimplement the theory of rationality expounded by Pollock's book without running afoul of the patent on specific algorithms. Of course, it may be cheaper and easier to just get a license from Dr. Pollock. Once again, I have done none of the above: I haven't even downloaded the OSCAR code due to a desire not to conflate anything I might choose to do with the OSCAR theory with use of the OSCAR algorithms or code.
I'm also at the very beginnings of some interesting investigations into trust metrics, in which I expect to leverage Raph's kind contributions to the public domain. No doubt I'll have questions later. Right now I'm too ignorant to have any questions—I'm too busy brushing up on my math. Here's what I'm going through, roughly in chronological order:
- Calculus Made Easy
- Concrete Mathematics: A Foundation for Computer Science (2nd Edition)
- Randomized Algorithms
Hopefully next on my reading list is Linear Algebra: A Modern Introduction. Any reviews before I purchase the text would be greatly appreciated.
10:24:54 AM 
|
|
