Lambda the Ultimate

ObjectiveCLIPS, a programming environment specifically designed for Cocoa, the native Mac OS X object system, has been updated to version 1.7. The new release includes a number of significant performance improvements along with a new execution trace feature that provides extensive logging of trace information during development.

ObjectiveCLIPS integrates the popular NASA-developed CLIPS expert system shell with Apple's Core Data technology and F-Script, allowing the creation of intelligent Cocoa applications with persistent object models and complex business rules. Developers can easily embed ObjectiveCLIPS in their application and take advantage of its powerful inference engine and associated tools to implement their application logic.

ObjectiveCLIPS unifies CLIPS facts with Core Data Objective-C objects, and allows for the manipulation of these objects with the Cocoa-based F-Script language in rules. By bringing the latest innovations in Mac OS X and object-oriented scripting together with the power of the CLIPS artificial intelligence environment, ObjectiveCLIPS provides a unique foundation for building smart Mac OS X applications.

ObjectiveCLIPS is open source software. It can be downloaded from http://www.ObjectiveCLIPS.com

Lately I have been coming across a set of ideas which seem to be related:
Logic/constraint/relational programming, unification, back tracking, business rules, logic variables, Gentzen, sequent calculus and so on.

Is there a comprehensive introduction to all of the above? I would like to know the meaning of the terms mentioned above and, if possible, how to implement them.

Krishnamurthi's book Programming Languages: Application and Interpretation mentions prolog, but doesn't show how to implement those ideas in scheme. The Reasoned Schemer is not easy to follow (due to the style of the book). It is not the kind of book one can read once a week after work. There are a few constraint logic books on Amazon, but I obviously don't even know enough to understand if they are good introductions.

There is a lot of talk of how functional programs operate at a higher level of abstraction (compared to imperative programs)...don't these logic/constraint programs operate at an even higher abstraction? Lisp defenders always make sure newbies understand that Lisp is not just for AI. Is the same true of prolog? I have read that logic programs are not very efficient; however, if they are related to relational databases (as claimed somewhere), then can't an 'index' be added to a list of 'facts' to make sure logic program's operation is as efficient as any other program?

I'm just trying to get a sense of the field, its benefits, its pitfalls and reasons why it is not so popular. Thanks.

Reading Martin Oderski's paper Scalable Component Abstractions, I ran across citations to the languages CeasarJ and Gbeta, both realizing a concept called virtual classes. This concept is explained, and a calculus given in the paper A Virtual Class Calculus by Erik Ernst, Klaus Ostermann, and William R. Cook.

Virtual classes are class-valued attributes of objects. Like virtual methods, virtual classes are defined in an object's class and may be redefined within subclasses. They resemble inner classes, which are also defined within a class, but virtual classes are accessed through object instances, not as static components of a class. When used as types, virtual classes depend upon object identity -- each object instance introduces a new family of virtual class types. Virtual classes support large-scale program composition techniques, including higher-order hierarchies and family polymorphism. The original definition of virtual classes in BETA left open the question of static type safety, since some type errors were not caught until runtime. Later the languages Caesar and gbeta have used a more strict static analysis in order to ensure static type safety. However, the existence of a sound, statically typed model for virtual classes has been a long-standing open question. This paper presents a virtual class calculus, VC, that captures the essence of virtual classes in these full-fledged programming languages. The key contributions of the paper are a formalization of the dynamic and static semantics of VC and a proof of the soundness of VC.